Tutorials
(Joint Tutorials with SAT and DIFTS)| Speaker | Affiliation | Tutorial Title | Slides |
| Andre Platzer | Carnegie Mellon University | Proving Hybrid Systems | [Slides] |
| Priyank Kalla | University of Utah | Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation | [Slides] |
| Roderick Bloem | Graz University of Technology | Reactive Synthesis | |
| Işil Dillig | The University of Texas at Austin | Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis | [Slides] |
Abstracts
Title: Proving Hybrid SystemsSpeaker: Andre Platzer
Abstract:
Cyber-physical systems (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which arise frequently in many safety-critical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another one?
This tutorial focuses on the most elementary CPS model: hybrid systems, which are dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. It describes a compositional programming language for hybrid systems and shows how to specify and verify correctness properties of hybrid systems in differential dynamic logic. Extensions of this logic that support CPS models with more general dynamics will be surveyed briefly.
In addition to providing a strong theoretical foundation for CPS, differential dynamic logics have also been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, several automotive systems, mobile robot navigation with the dynamic window algorithm, and a surgical robotic system for skull-base surgery. The approach is implemented in the theorem prover KeYmaera X.
Speaker Bio.:André Platzer is an Associate Professor of Computer Science at Carnegie Mellon University. His interests include logic in computer science, cyber-physical systems, programming languages, formal methods, and automated theorem proving. He received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, the Best Paper Awards at TABLEAUX'07 and at FM'09. André Platzer was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009 and one of the AI's 10 to Watch 2010 by the IEEE Intelligent Systems Magazine.
Title: Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation
Speaker: Priyank Kalla
Abstract:
Click here for the talk abstract.
Speaker Bio.:Priyank Kalla received the Bachelors degree in electronics engineering from Sardar Patel University, in 1993, and MS and PhD degrees from the Univ. of Massachusetts Amherst in 1998 and 2002, respectively. Since 2002, he has been a faculty member at the ECE department at the Univ. of Utah. He has also worked at Advanced Micro Devices and the Digital Equipment Corporation (Alpha CAD & Test group). His areas of interest are in Electronic Design Automation and Hardware Verification. He was the chair of the IEEE Technical Committee on Computer-Aided Network Design (CANDE) 2012, and the General Chair of IEEE High-Level Design Validation and Test Workshop (HLDVT) 2009. He is a recipient of the US National Science Foundation Faculty Early Career Development (CAREER) Award, and the ACM Trans. on Design Automation 2009 best paper award.
Title: Reactive Synthesis
Speaker: Roderick Bloem
Abstract:
Synthesis is the question of how to construct a correct system from a specification. In recent years, synthesis has made major steps from a theoretist’s dream towards a practical design tool. While synthesis from a language like LTL has very high complexity, synthesis can be quite practical when we are willing to compromise on the specification formalism. Similarly, we can take a pragmatic approach to synthesize small distributed systems, a problem that is in general undecidable.
Speaker Bio.:Roderick Bloem received an MS in computer science from Leiden University in the Netherlands (1996) and a PhD from the University of Colorado at Boulder (2001). His thesis work, under the supervision of Fabio Somenzi, was on formal verification using Linear Temporal Logic.
Since 2002, he has been an assistant professor at Graz University of Technology and a full profesor since 2008. His research interests are in formal methods for the design and verification of digital systems, including hardware, software, and combinations such as embedded systems. He studies applications of game theory to the automatic synthesis of systems from their specifications, connections between temporal logics and omega-automata, model checking, and automatic fault localization and repair.
Title: Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis
Speaker: Işil Dillig
Abstract:
Abductive inference is a form of backwards logical reasoning that infers likely hypotheses from a given conclusion. In other words, given an invalid implication of the form A => B, abduction asks the question "What formula C do we need to conjoin with the antecedent A so that (i) A & C => B is logically valid and (ii) C is consistent with A?" Abductive reasoning has found many applications in program verification and synthesis, particularly in modular program analysis, invariant generation, and automated inference of missing program expressions. This tutorial will give an overview of logical abduction and algorithms for performing abductive inference. We will also survey several use cases of abductive inference in the context of program analysis, verification, and synthesis.
Speaker Bio.:Işil Dillig is an Assistant Professor of Computer Science at the University of Texas at Austin. She is also a Sloan Fellow and a recipient of the NSF CAREER award. She obtained all her degrees (BS, MS, PhD) from Stanford University. Prior to joining UT Austin, Dr. Dillig worked as a researcher at Microsoft Research (2013-2014) and as an assistant professor of computer science at the College of William & Mary (2012-2013).