Software Reliability and Constraint Solving Workshop
Date: 8 March 2017
Location: EPFL, BC 410
09:30. Rustan Leino: Well-founded functions, induction, and extreme predicates in an SMT-based verifier
An SMT solver takes first-order formulas as input and provides impressive automation. But what if the problem at hand goes beyond first order? The Dafny program verifier provides well-founded functions, inductive proofs, and predicates defined as least and greatest fixpoints. It encodes properties of these into first-order logic in such a way that harnesses the automation of SMT solvers. In this talk, I will give an overview of functions and induction in Dafny, and will then focus on the encoding on predicates defined by fixpoints.
Bio: Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. He is an ACM Fellow. Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he likes to cook and, being a multi-instrumentalist, play music. Leino instructed group cardio and strength classes for many years, he more recently danced on a salsa performance team, and he once needed a helicopter to get off a Swiss mountain.
11:00. Sergio Giro: Verification of distributed probabilistic systems under partial information
In the verification of systems that involve probabilities, it is crucial to study qualitative properties concerning the probability of certain events as, for instance, 'the probability that a failure occurs is less that 0.01'. In case the system under consideration is distributed, each of the components of the system might have a partial view of the information available to other components. The analysis of these systems is carried out by considering 'distributed adversaries' with restricted observations. In this talk I will summarise six years of research on automatic verification of distributed probabilistic systems. On the negative side, we proved the verification problem to be undecidable in general and NP-complete for some restricted systems. Nevertheless, we also introduced some techniques for overestimation of worst-case probabilities, and showed that the concept of distributed adversaries can be used to improve existing techniques such as partial order reduction.
Bio: Sergio holds an MSc and a PhD in Computer Science, both obtained at National Universities in Argentina, with a strong focus on formal methods, logic and compilers. After serving as a Research Assistant in Oxford University in the area quantitative analysis of distributed systems, he joined Google for 4 years, working on distributed data processing and analysis applied to a variety of problems including demand forecast, fraud detection and development of Java security libraries for Android.
14:00. Nikolaj Bjørner: Programming Constraint Services with Z3
Many program verification, analysis, testing and synthesis queries reduce to solving satisfiability of logical formulas. Yet, there are several applications where satisfiability, and optionally a model or a proof, is insufficient. Examples of useful additional information include interpolants, models that satisfy optimality criteria, generating strategies for solving quantified formulas, enumerating and counting solutions. We will cover some of the newer features in Z3 that expose constraint services. For applications in product configuration, Z3 includes specialized solvers for finding backbones under assumptions, for solving quantified formulas Z3 contains elements of partial quantifier elimination methods based on models, and for solving optimization modulo SMT, Z3 contains dedicated MaxSMT.
Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work with Leonardo de Moura and Christoph Wintersteiger is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS in 2014. Previously, he developed the DFSR, Distributed File System - Replication, and Remote Differential Compression protocols, RDC, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first few years of university at DTU and DIKU.
15:30. Philippe Rümmer: The Quest for Systematic Predicate Abstraction
Heuristics for discovering predicates for abstraction are an essential part of CEGAR-based software model checkers or Horn solvers. Picking the right predicates affects the runtime of a model checker, or determines if a model checker is able to solve a verification task at all. This talk will summarise some of our research on how to choose predicates in a systematic way. The first part of the presentation will explain how Craig interpolation, one of the standard methods for refining abstractions, can be adapted to take program-specific information or refinement heuristics into account. The second part will present different methods to actually generate such program-specific information: with the help of upfront static analysis of a program, using domain-specific acceleration techniques, or using type-based analysis to extract variable roles.
Joint work with Yulia Demyanova, Jérôme Leroux, Pavle Subotic, and Florian Zuleger.
Bio: Philipp Ruemmer is an assistant professor at Uppsala University, Sweden. He received his doctorate in Computer Science from Chalmers University and Gothenburg University in 2008. Before joining Uppsala University as an assistant professor, he has been research assistant at the Oxford University Computing Laboratory. His research interests include various directions in program verification, theorem proving and SMT reasoning, and application of such methods in the area of embedded systems. Philipp received the Oscar Prize of Uppsala University in 2013, for contributions to the field of program correctness, and the IJCAR best paper award in 2014; the theorem prover Princess resulting from his research won the TFA division of the theorem proving competition CASC in 2012.
16:30. Bruno Marnette: On the Real Expressive Power of Datalog Extensions
Numerous extensions of the Datalog language have been introduced to address the lack of expressive power of traditional Datalog. In particular, equality constraints and value invention have proven convenient in the context Data Exchange and DL-like reasoning. Adding such constraints to the Datalog language however leads to intractability, and a great amount of work has aimed at identifying tractable islands, typically relying on syntactic properties (such as acyclicity or guardedness). In this talk we'll investigate whether the theoretic expressive power of these tractable extensions truly differ from standard Datalog. (Spoiler alert: they don't).
Bio: Dr. Bruno Marnette is the CEO of Prodo and CTO of Enki. Previously, he worked at Palantir and was a post-doctoral researcher at ENS/INRIA. Bruno holds PhD from Oxford University.