Date: 8 March 2017

Location: EPFL, BC 410

Speakers:

• Nikolaj Bjørner
• Sergio Giro
• Rustan Leino
• Bruno Marnette
• Philippe Rümmer

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.

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.

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.

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.

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