Seminar Series by Ruzica Piskac
Ruzica Piskac
Max Planck Institute for Software Systems
Program verification using SMT Solvers
Date: Monday, September 24th, 2012
Time: 5PM
Venue: CS10.Abstract:
Software verification is a formal proof of the correctness of program, with respect to a certain property. In this tutorial we will introduce through examples basic terminology in software verification, such as verification conditions, pre- and post-conditions, Hoare triples. We well also show how verification relies on the use of SMT solvers. Modern SMT solvers are powerful tools, used as a core engine in applications, such as program analysis, software engineering, program model checking, hardware verification, and many more. In this talk we give an overview of basic techniques, used in the implementation of SMT solvers. SMT solvers can reason about formulas that combine several different theories and we describe the standard Nelson-Oppen combination procedure.
Reasoning about collections with cardinality constraints
Date: Tuesday, September 25th, 2012
Time: 5PM
Venue: CS101.Abstract:
Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the content of linked data structure with duplicate elements leads to multisets. Interactive theorem provers such as Isabelle specify theories of multisets and prove a number of theorems about them to enable their use in interactive verification. However, the decidability and complexity of constraints on multisets is much less understood than for constraints on sets.
In this talk we will show that the satisfiability problem for a logic of sets, multisets (bags), and cardinality constraints is decidable. We will also show that the optimal complexity results. It relies on an extension of integer linear arithmetic with a "star" operator, which takes closure under vector addition of the solution set of a linear arithmetic formula. We show that the satisfiability problem for this extended language remains in NP (and therefore NP-complete). Our proof uses semilinear set characterization of solutions of integer linear arithmetic formulas, as well as a generalization of a recent result on sparse solutions of integer linear programming problems.
Software Synthesis using Automated Reasoning
Date: Wednesday, September 26th, 2012
Time: 5PM
Venue: CS101.Abstract:
Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier, while increasing both the productivity of the programmer and the correctness of the produced code. In this talk I will present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First I will describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. I will illustrate the process of turning a decision procedure into a synthesis procedure using linear integer arithmetic as an example. This approach is implemented in Comfusy. Comfusy is an extension to the Scala compiler and a tool for complete functional synthesis. It accepts as an input expressions with input and output variables and outputs code that computes output values as a function of input values. In addition, it also outputs the preconditions that the input variables have to satisfy in order for a solution to exist. Next I will outline a synthesis procedure for specifications given in the form of type constraints. The procedure derives code snippets that use given library functions. The procedure takes into account polymorphic type constraints as well as code behavior.We implemented this approach in a tool called Insynth. To help developers in composing functionality from existing libraries and from the user defined values, InSynth synthesizes and suggests valid expressions of a given type at a given program point.
About the speaker:
Ruzica Piskac is faculty at the Max Planck Institute for Software Systems (MPI-SWS) and head of the Synthesis, Analysis and Automated Reasoning Group. Prior to joining MPI-SWS, she was a graduate student at the EPFL (2007-2011), where she worked under the supervision of Viktor Kuncak.
Her research interests span the areas of software verification, automated reasoning, code synthesis and program termination. A common thread in her research is improving software reliability and trustworthiness using formal techniques.