Schedule

Tuesday
SAT Day
Wednesday
SMT Day
Thursday
AR Day
Friday
Computer Algebra
and Applications Day
9:00 Welcome session Session 5:
Alberto Griggio
Introduction to SMT
Session 9:
Uwe Waldmann
Saturation Theorem
Proving
Session 13:
Arie Gurfinkel
Solving Constrained
Horn Clauses
9:30 Session 1:
Armin Biere
Encoding into SAT
10:00
10:30 Coffee break Coffee break Coffee break
11:00 Coffee break Session 6:
Pascal Fontaine
Quantifiers in SMT
Session 10:
Stephan Schulz
Implementation of
Saturating Theorem
Provers
Session 14:
John Abbott
Introduction to Symbolic
Computation: polynomials
and ideals
11:30 Session 2:
Gilles Audemard
CDCL and Parallel SAT
12:00
12:30 Lunch Lunch Lunch
13:00 Lunch
13:30 Session 15:
Matthew England
Cylindrical Algebraic
Decomposition
14:00 Session 3:
Practical SAT Session
Session 7:
Aina Niemetz
Mathias Preiner
SMT in Practice
Session 11:
Martin Suda
Playing with Vampire –
the dark art of
theorem proving
14:30
15:00 Coffee break
15:30 Coffee break Coffee break Coffee break Session 16:
Philipp Rümmer
SMT solving for strings
and security
16:00 Session 4:
Marijn Heule
Preprocessing and
Inprocessing
Session 8:
Martin Brain
Bit-Exact Automated
Reasoning About Floating
Point Arithmetic
Session 12:
Laura Kovacs
First-order Interpolation
16:30
17:00
17:30 Reception
Christies
18:00
18:30 Dinner
MOSI
19:00
19:30
20:00
20:30

SAT Sessions

Session 1: Encoding into SAT (Armin Biere)

We first discuss conjunctive normal form (CNF) and alternatives and then how to translates various problems into CNF through intermediate formats including bit-vectors, negation normal form, circuits and AIGs. We touch on encoding logical constraints and various software engineering challenges in this process too. Finally we explain input formats of SAT solvers and dwell on incremental usage through APIs.

See Armin’s page for slides and material.

Session 2: CDCL and Parallel SAT (Gilles Audemard)

In this tutorial, we will focus on sequential and parallel SAT solving techniques. We will first describe the main components of Conflict Driven Clause Learning (CDCL) architecture used in most SAT solvers (conflict analysis, restarts, heuristics…). After that, we will present different approaches used to solve SAT in a parallel environment with a special attention to shared clauses.

Slides and other material.

Session 3: Practical SAT Session (Armin Biere, Gilles Audemard, Marijn Heule)

See practical session page.

Session 4: Preprocessing and Inprocessing (Marijn Heule)

The success of modern SAT solvers depends strongly on their ability to simplify the given formula. Simplification can substantially reduce the size of formulas and fix poor encodings automatically. The first important simplification technique was variable elimination and is now used by practically all SAT solvers. Simplification techniques were initially only applied before the search as a preprocessing step. Today, several state-of-the-art solvers use inprocessing: alternate between search and simplification. Inprocessing can boost performance on various application, including hardware and software verification. The tutorial will cover a high-level overview of preprocessing and inprocessing in state-of-the-art solvers as well as a description of the six mostly-used simplification techniques.

Slides.

SMT Sessions

Session 5: Introduction to SMT (Alberto Griggio)

The tutorial will provide an introduction to the SMT problem and the main techniques for solving it. We will describe the basic components of modern SMT solvers, their underlying algorithms and relevant implementation aspects, and show how they are used for implementing efficient decision procedures for various theories of practical interest. Most of the focus will be on the DPLL(T) approach to SMT, but we will also briefly look at alternative techniques and current trends.

Session 6: Quantifiers in SMT (Pascal Fontaine)

In this lecture, we will review the current methods to handle quantifiers in Satisfiability Modulo Theories (SMT) solvers. We assume knowledge of SMT for handling ground formulas. We will first study the theoretical grounds for quantifier handling in SMT, that is, for instantiation. Then, the main techniques for instantiation in state-of-the-art SMT solvers will be presented: e-matching or trigger-based instantiation, model-based quantifier instantiation, conflict-based and enumerative instantiation.

Slides.

Session 7: SMT in Practice Part (Aina Niemetz and Mathias Preiner)

In this session, we will give a hands-on introduction to SMT solvers. We will assist the participants in installing and setting up the required tools. Alternatively we will provide a ready-to-use virtual machine. We will cover basic SMT concepts, which the participants will then apply to various exercises.

Session 8: Bit-Exact Automated Reasoning About Floating-Point Arithmetic (Martin Brain)

The majority of new instrumentation and control systems, even those that are safety critical, make use of floating-point numbers. So the value of computer-generated assurance evidence (including verification, test coverage, etc.) depends on the correctness, completeness and efficiency of automated reasoning about floating-point expressions. This session will cover the challenges of reasoning about floating-point, the SMT-LIB Theory of Floating-Point with its semantics and the rationale behind key design decisions as well as surveying the current state-of-the-art in solver technology and future research directions. I aim to provide system integrators with sufficient information to integrate floating-point support into SMT interfaces and solver developer enough ideas to work on the next generation of floating-point reasoning.

Slides.

Automated Resoning Sessions

Session 9: Saturation Theorem Proving (Uwe Waldmann)

Automated theorem provers have become increasingly important for improving the degree of automation of interactive proof systems. Saturation provers, such as E, SPASS, or Vampire, are one of the two categories of automated provers used in this context. These provers are based on variants of the superposition calculus for (uninterpreted) first-order logic with equality. In this lecture, we give an overview of the history of saturation calculi from the 1960’s (resolution, completion) to recent developments; we explain how these calculi work, why they work, and what makes them successful in practice.

Slides

Session 10: Implementation of Saturating Theorem Provers (Stephan Schulz)

We will describe several aspects of the implementation of a saturating, superposition-based theorem prover for first-order logic. We discuss the basic architecture of a prover, and the organization of the actual proof search via the given-clause algorithm. Simplification and redundancy elimination are, in practice, critical, and we describe how these can be integrated into the basic proof procedure.

Another topic is that of terms and clauses, the most basic data objects in any prover, and how they can be implemented. We discuss bottlenecks of naive implementations, as well as the principle and some examples of indexing techniques to overcome these bottlenecks. The presentation concludes with a look at the influence of search heuristics.

Slides

Session 11: Playing with Vampire – the dark art of theorem proving (Martin Suda)

This talk will follow the theoretical sessions by Uwe and Stephan and complement them by a hands on experience with the leading automatic theorem prover Vampire. The participants will get assistance in installing Vampire and the lecture will cover the main features of the prover and how they can be used in various application domains.

Session 12: First-order Interpolation (Laura Kovacs)

Craig Interpolation is an important technique in computer aided verification and static analysis of programs. In particular, interpolants extracted from so-called local proofs are used in invariant generation and bounded model checking. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. In this talk we first describe a technique of generating and optimizing interpolants based on transformations of what we call the “grey area” of local proofs. Local changes in proofs can change the extracted interpolant. Our method can describe properties of extracted interpolants obtained by such proof changes as a pseudo-boolean constraint. By optimizing solutions of this constraint we also improve the extracted interpolants. While local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs. In this talk we therefore also investigate interpolant extraction from non-local proofs in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants.

Slides and examples

Computer Algebra and Applications Sessions

Session 13: Solving Constrained Horn Clauses with SMT (Arie Gurfinkel)

The logic of Constrained Horn Clauses (CHC) provides an effective logical characterization for many software verification problems including safety verification via inductive invariants, inter-procedural analysis with function summaries, compositional verification of concurrent systems, modular verification of distributed systems, and verification of program equivalence. CHC are used as an intermediate representation by several verification framework including SeaHorn, JayHorn, Eldarica, and ARMC. In this talk, I will give an overview of Spacer — an SMT-based procedure for deciding satisfiability of CHC. Spacer extends the powerful IC3 framework from Hardware Model Checking to SMT. This requires significant modifications both to the original IC3 algorithm and to capabilities offered by an SMT solver. Spacer is the main verification engine of the C/C++ verification framework SeaHorn and several other tools.

Slides

Session 14: Introduction to Symbolic Computation – polynomials and ideals (John Abbott)

We give a quick overview of some of the main precepts of symbolic computation including unlimited precision, exact arithmetic (as opposed to approximate floating-point arithmetic), and the representation of polynomials. We recall that a “polynomial ideal” is a mathematically rich way to represent systems of polynomial equations; and that a Groebner basis is a computationally rich way of representing a polynomial ideal. The notions in the presentation will be illustrated by various examples (using the CoCoA computer algebra system).

Slides and example

Session 15: Symbolic Computation – Cylindrical Algebraic Decomposition (Matthew England)

This session will focus on Cylindrical Algebraic Decomposition (CAD). CAD has long been a topic of study within Symbolic Computation as a tool to perform quantifier elimination over the reals. CAD (and the underlying technology) has found renewed interest recently as the SMT community have engaged it for use with non-linear real arithmetic. We will review the original CAD algorithm; the most important advances in CAD theory since its inception; and recent links with Satisfiability Checking and SMT. Time permitting the author will describe some of his recent work including: adaptations to the core CAD algorithm to take advantage of the logical structure in problems; man made and machine learned heuristics for optimising CAD settings; applications in bio-chemical systems, economic reasoning and computation with multi-valued functions.

The speaker is funded by EU Horizon 2020 Project SC-Square which seeks to bridge the two communities of Symbolic Computation and Satisfiability Checking.

Slides

Session 16: SMT solving for strings and security: an overview (Philipp Rümmer)

The recent years have seen a wealth of research on string solvers, i.e., SMT solvers that can efficiently check satisfiability of quantifier-free formulas over a background theory of strings and regular expressions. String solvers can be applied in a variety of verification approaches, for instance in software model checking to take care of implication and path feasibility checks; the most widespread adoption has occurred in the area of security analysis for languages like JavaScript and PHP, for instance to discover information leaks or vulnerability to injection attacks. To process constraints from those domains, it is necessary for string solvers to handle a delicate combination of (theoretically and practically) highly challenging operations: concatenation in word equations, to model assignments in programs; regular expressions or context-free grammars, to model properties or attack patterns; string length, to express string manipulation in programs; transduction, to express sanitisation, escape operations, and replacement operations in strings; and others. The lecture will give an overview of the application of string solvers for security properties, but also explain properties of the theory and different solver architectures.

Slides

Reception

The reception will take place in Christie’s Bistro located in the Library of Owen’s College at the university.

Dinner

The dinner will be at the Museum of Science and Engineering (MOSI) located in the south-western city centre.

Detailed instructions coming soon!