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.

ABSTRACT. Algebraic geometry is the study of the geometry of solutions to a system of multivariate polynomial equations. Modern algebraic geometry does not explicitly solve the system of equations to enumerate the solutions, but rather reasons about the presence, absence, dimensions or intersection properties of the solution-sets, etc. Abstract and computational algebra is often used for this purpose – particularly the theory and technology of Grobner bases, which provides a very powerful set of tools to solve many polynomial decision problems. In this talk, I will present a tutorial on how some of these techniques from algebraic geometry and commutative algebra can be used for formal verification of RTL datapaths and arithmetic circuits.

While Grobner basis techniques are very powerful, the computation suffers from high complexity. Therefore, the main focus of the tutorial will be on how to overcome this complexity. I will describe: • How to formulate various verification problems using ideal membership, Nullstellensatz, elimination theory and Grobner bases; • How to exploit the number-theoretic properties of finite rings and fields to simplify the problems; • How to analyze the structure/topology of the given circuits to get more theoretical insights into the corresponding polynomial ideals, and use this information to improve the computation; and • How to implement the aforementioned concepts using modern symbolic computation algorithms, e.g. Faugere’s F4-style reductions, for practical datapath verification.

Arithmetic datapaths are usually custom designed, and they often exhibit some structure or symmetry in the implementations. Grobner bases can help identify this inherent symmetry. By exploiting this information, efficient symbolic computation algorithms can then be devised for scalable verification. The verification context will be motivated by applications such as elliptic curve cryptography, error correcting circuits, polynomial signal processing, word-level RTL synthesis, etc. I will provide information on various resources – publications, design benchmarks and the verification tools developed by us – so that interested participants can explore this exciting area of work. I will conclude by describing important unsolved problems in this specific area, and the challenges that need to be overcome to fully exploit the potential of the theory and technology.

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.

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.

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).