Loading Events « Back to Events
Levine 307
220 S 33rd St, Philadelphia, Pennsylvania , United States

Upcoming Events At This Venue

October 8, 2012


Quantitative verification techniques are able to establish system properties such as “the probability of an airbag failing to deploy on demand” or “the expected time for a network protocol to successfully send a message packet”. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behavior. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyze abstractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modeling language.

This is joint work with Gethin Norman and David Parker.


Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She was elected to Academia Europea and received a prestigious ERC Advanced Grant VERIWARE “From software verification to everyware verification”, 2010-15.

Kwiatkowska’s research is concerned with modeling and verification techniques for probabilistic systems, with application to engineered and biological systems. She spearheaded the development of probabilistic and quantitative methods in verification on the international scene. Her work on the theory to practice transfer of probabilistic model checking was recognized by invitations to speak at the LICS 2003 and ESEC/FSE 2007 conferences. She led the development of the PRISM model checker, the leading software tool in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management and systems biology. Her research is currently supported by £3.7m of grant funding from EPSRC, EU, DARPA, Oxford Martin School and Microsoft Research.

Kwiatkowska serves on editorial board of IEEE Transactions on Software Engineering, Philosophical Transactions of the Royal Society A and Science of Computer Programming, and has lectured at several summer schools, including ESSLLI and the Marktoberdorf Summer School.

Date: October 8, 2012 @ 2:00 pm

February 5, 2013

PRECISE Seminar:
Toyota’s Advanced Driver Assist System (ADAS)

Mr. Tomoo Kakegawa & Atsushi Hayashi
Vehicle Control System Infrastructure Development Division

The demand of higher driving safety is increasing. Several driving assistance systems, e.g., PCS (Pre-Crash safety System), LKA (Lane Keep Assist) are already available in the market. However, highly advanced and integrated safety system: Advanced Drive Assist System is necessary in the future. In order to achieve this goal, there are several challenging problems: architecture design exploration, design methodologies and tools, and security. In this talk, we will talk about our ongoing project of a new ADAS and open questions.

Date: February 5, 2013 @ 11:00 am

March 28, 2013

The tentative schedule:

– 10-10:30 am: welcome and overview
– 10:30-noon: presentations on control design and challenge problem
– noon-1pm: lunch
– 1pm-2pm: presentations on code generation and analysis
– 2pm onwards: discussions and feedback
Date: March 28, 2013

May 29, 2013

PRECISE Seminar: Allocation, Isolation, & Dynamics in Compositional Real-Time Systems & Applications to Control System Design

Nathan Fisher, Ph.D.,
Wayne State University

Abstract: The recent focus upon compositional design in real-time systems research has yielded a number of promising frameworks for the integration of multiple safety- and time-critical components upon a shared computational platform.  Integration of components has a profound impact upon the size and cost of the system by potentially reducing the hardware resources that must be dedicated to ensure the safe functioning of the system.  These frameworks have also introduced many interesting open research challenges such as: 1) Allocation: how do we determine the optimal interface which accurately describes the temporal requirements of a component; 2) Isolation: how can components be isolated from the temporal faults or misbehavior of other components; 3) Dynamic Behavior: how do components adaptively change their behavior in response to a dynamic environment.

In this talk, I describe our recent work on the above challenges via the development of efficient schedulability analysis that provides formal guarantees on the temporal correctness of compositional real-time systems.  Furthermore, each of our solutions is either provably optimal or has bounded deviation from the optimal solution.  The existence of such optimality guarantees imply our solutions may be leveraged in reducing the size, weight, and power (SWaP) requirements of safety-critical real-time systems that employ component-based design.  Finally, I will discuss some surprising applications of our obtained solutions to the area of thermal-aware real-time control system design.


Biography: Nathan Fisher is an Assistant Professor in the Department of Computer Science at Wayne State University.  He received his Ph.D. from the University of North Carolina at Chapel Hill in 2007, his M.S. degree from Columbia University in 2002, and his B.S. degree from the University of Minnesota in 1999, all in computer science.   His research interests are in real-time and embedded computer systems, sustainable computing, resource allocation, game-theory, and approximation algorithms.  His current funded research projects are on composability of real-time applications, multiprocessor real-time scheduling theory, thermal-aware real-time system design, and algorithmic mechanism design in competitive real-time systems.  He received  the NSF CAREER Award in 2010 and best paper awards from publication venues such as RTSS, ECRTS, and IEEE Transactions on Industrial Informatics.

Date: May 29, 2013 @ 11:30 am

August 13, 2013

PRECISE Seminar: Cyber-Physical Systems:  Continuity and Transitions

Helen Gill, Ph.D.,
National Science Foundation

Abstract: This talk takes a retrospective look at the course of Cyber-Physical Systems, and then looks forward to challenges ahead.  There have been changes, and more are coming  –  some seen, some doubtless not anticipated.  But the need for, and interest in, the CPS area is only growing.  As researchers gravitate to this field, they will find opportunities to tackle new and interesting problems, both in the application domains and in the science and technology.

Biography: Dr. Helen Gill is the Program Director for the Embedded & Hybrid Systems program of the National Science Foundations Directorate for Computer and Information Science and Engineering (CISE) Division of Computer and Network Systems (CNS). Previously, she served as a Program Manager in the Information Technology Office of the Defense Advanced Research Projects Agency, where she developed programs in software-enabled control and hybrid systems and in programming technology for embedded systems.

At DARPA she also managed research in modeling and formal methods for software development and evolution. Previously she was a Principal Scientist with the MITRE Corporation and directed the National Science Foundation programs in Software Engineering and Programming Languages.

Dr. Gill received her B.A. degree in Mathematics from the University of Missouri (General Honors), M.S. in Computer Science from the University of Colorado, and Ph.D. in Computer Science from Auburn University. She is a member of Phi Beta Kappa. Her academic honors include Pi Mu Epsilon; Phi Kappa Phi; MU Curators, Powell B. McHaney, Burroughs, and CU Regents Fellowships. Her research publications are in graph decomposition for concurrency analysis, partitioning and scheduling software for parallel execution, distributed programming environments, and discrete event simulation. Her current research interests are in software for embedded systems, middleware, hybrid discrete and continuous systems, software analysis, applied formal methods, and technology for high confidence software and systems. She co-chairs coordinating group for High Confidence Software and Systems under the auspices of the Interagency Working Group for ITR&D.

Date: August 13, 2013 @ 11:30 am

October 9, 2013

Date: October 9, 2013 @ 6:00 pm

January 27, 2014

PRECISE Seminar: Modular Reasoning about Heap Paths via Effectively Propositional Formulas

Shachar Itzhaky, Tel Aviv University

Abstract: First order logic with transitive closure, and separation logic enable elegant interactive verification of heap-manipulating programs. However, undecidabilty results and high asymptotic complexity of checking validity preclude complete automatic verification of such programs, even when loop invariants and procedure contracts are specified as formulas in these logics. This work tackles the problem of procedure-modular verification of reachability properties of heap-manipulating programs using efficient decision procedures that are complete: that is, a SAT solver must generate a counterexample whenever a program does not satisfy its specification. By (a) requiring each procedure modifies a fixed set of heap partitions and creates a bounded amount of heap sharing, and (b) restricting program contracts and loop invariants to use only deterministic paths in the heap, we show that heap reachability updates can be described in a simple manner. The restrictions force program specifications and verification conditions to lie within a fragment of first-order logic with transitive closure that is reducible to effectively propositional logic, and hence facilitate sound, complete and efficient verification. We implemented a tool atop Z3 and report on preliminary experiments that establish the correctness of several programs that manipulate linked data structures.

Biography: Shachar took his undergraduate studies in computer science at the Open University, and then entered a Master program at Tel Aviv University under the supervision of Prof. Mooly Sagiv. His Master thesis was a simple method for inductive synthesis of short code fragments with applications to finite differencing. After obtaining a Master’s degree he continued as a graduate student under the supervision of Prof. Sagiv, in the area of automated software verification.

Date: January 27, 2014 @ 1:00 pm

February 5, 2014

PRECISE Seminar: Microfabricated Implantable Wireless Microsystems: Permanent and Biodegradable Implementations

Mark Allen, Ph.D.,
Alfred Fitler Moore Professor and Director
Singh Center for Nanotechnology
University of Pennsylvania

Abstract: The tremendous technological convergence of microfabrication technology, wireless communication technology, and low-power circuitry has opened the possibility of widespread use of microfabricated implantable wireless microsystems. A typical operational mode for these microsystems is to transduce a physiological parameter relevant to a disease state of interest, and wirelessly communicate this parameter external to the body to guide therapy. For chronic disease states, long-term, permanent sensors are of interest; while for acute disease states, biodegradable wireless microsystems may be of interest. Two microsystem examples, permanent pressure sensors for chronic monitoring of patients with congestive heart failure, and biodegradable pressure sensors for acute monitoring of patients with transient conditions, are given.

Biography: Mark G. Allen received the B.A. degree in chemistry, the B.S.E. degree in chemical engineering, and the B.S.E. degree in electrical engineering from the University of Pennsylvania, Philadelphia, and the S.M. and Ph.D. (1989) degrees from Massachusetts Institute of Technology, Cambridge. In 1989 he joined the faculty of the School of Electrical and Computer Engineering, Georgia Institute of Technology, Atlanta, ultimately holding the rank of Regents’ Professor and the J.M. Pettit Professorship in Microelectronics, as well as a joint appointment in the School of Chemical and Biomolecular Engineering. In 2013 he left Georgia Tech to become the Alfred Fitler Moore Professor of Electrical and Systems Engineering and Scientific Director of the Singh Nanotechnology Center at the University of Pennsylvania in Philadelphia, PA. His research interests are in the development and the application of new micro- and nanofabrication technologies, as well as MEMS. He was Editor-in-Chief of the Journal of Micromechanics and Microengineering from 2008-2013, co-chair of the IEEE MEMS Conference in 1996, co-chair of the Power MEMS conference in 2012, and will co-chair the 2016 Solid State Sensors Conference. He is co-founder of multiple companies, including Cardiomems and Axion Biosystems, and is a Fellow of the IEEE.

Date: February 5, 2014 @ 11:30 am

February 18, 2014

PRECISE Seminar: Computational Game Theory in Sequential Environments

Michael L. Littman,
Brown University

Abstract: Compared to typical single-agent decision problems, general sum games offer a panoply of strategies for maximizing utiity. In many games, such as the well-known Prisoner’s dilemma, agents must work together, bearing some individual risk, to arrive at mutually beneficial outcomes. In this talk, I will discuss several algorithmic approaches that have been developed to identify cooperative strategies in non-cooperative games. I will describe an analysis of value-function-based reinforcement learning, the pivotal role of assumptions about the opponent, the computational benefits of side payments, a multi-stage extension of the computational folk theorem, and the role of cognitive hierarchies.

Biography: Michael L. Littman’s research in machine learning examines algorithms for decision making under uncertainty. He has earned multiple awards for teaching and his research has been recognized with three best-paper awards on the topics of meta-learning for computer crossword solving, complexity analysis of planning under uncertainty, and algorithms for efficient reinforcement learning. Littman has served on the editorial boards for the Journal of Machine Learning Research and the Journal of Artificial Intelligence Research. He was general chair of International Conference on Machine Learning 2013 and program chair of the Association for the Advancement of Artificial Intelligence Conference 2013.

Date: February 18, 2014 @ 1:00 pm

February 21, 2014

PRECISE Seminar: Towards Mobile Sensing of Attention and Distraction

Marco Gruteser,
Rutgers University

Abstract: It has long been recognized that ubiquitous information access brings enormous benefits but also creates a plethora of devices and services that are competing for our attention. With mobile devices this is a particular serious concern for drivers, pedestrians, and other traffic participants, but understanding attention patterns can also be beneficial for entertainment services. In this talk, I will discuss our work towards mobile devices that can accurately track user attention – from devices that determine when we drive, over devices that recognize their users by touch, to devices that tracking what a users are looking or pointing at. These techniques can be expected to enable systems that help us better navigate distractions and understand what services and content capture our attention.

Biography: Marco Gruteser is an Associate Professor of Electrical and Computer Engineering at Rutgers University and a member of the Wireless Information Network Laboratory (WINLAB). He is a pioneer in the area of location privacy and also recognized for his work on connected vehicle applications. Beyond these topics, his more than hundred peer-reviewed articles and patents span a wide range of wireless, mobile systems, and pervasive computing issues. He received his MS and PhD degrees from the University of Colorado in 2000 and 2004, respectively, and has held research and visiting positions at the IBM T. J. Watson Research Center and Carnegie Mellon University. He is a member of the executive committee of ACM SIGMOBILE. His recognitions include an NSF CAREER award, a Rutgers Board of Trustees Research Fellowship for Scholarly Excellence, as well as best paper awards at ACM MobiCom 2012, ACM MobiCom 2011 and ACM MobiSys 2010. His work has been featured in numerous media outlets including the MIT Technology Review, NPR, the New York Times, and CNN TV.

Date: February 21, 2014 @ 1:00 pm
full screen background image