SAT/SMT solving (3 ECTS)

Note: the part SAT/SMT may be taken as a separate half course for ORCO students.

Context

Program testing and verification

_Testing_ is a well-known approach for ascertaining if a program works correctly: one runs the program, or parts thereof, on examples (hand-written or sometimes automatically generated) and checks that the output fits the specification. Even if there is no specification, it is at least implicit that the program should not crash.

Yet testing suffers from a major weakness: it checks a finite number of cases and a bug may be unnoticed if it is not triggered by any of these. _Symbolic testing_ was introduced: through _symbolic execution_ the program is executed with some of the input value kept symbolic: for instance instead of considering that input variable _x_ is 5 for testing, we will keep it symbolic and thus explore the code for all possible values of _x_. This is much more thorough than normal testing (also known as _concrete testing_), but also much more difficult to perform: the program may have to be explored through different paths, and sophisticated algorithms are used to check for infeasible paths. Since keeping everything symbolic is complicated and costly, and sometimes impossible (when executing system calls, for instance) most tools do a mixture of concrete and symbolic execution, also known as _concolic testing_.

In general, symbolic testing cannot _prove_ that a program will not encounter a bug, because of the possibly infinite number of execution steps to simulate. Proving that a program works as intended is actually much like proving mathematical theorems: one proves a property by induction on the number of steps that the program executes (or number of loop iterations, etc.). One important difficulty is that the property that can be proved by induction (known as an _inductive invariant_) is not necessarily the final property that we are interested in. Providing suitable inductive invariants is human intensive, and thus much work has been put into automating both finding such invariants and then proving that they are inductive.

Results from Turing (and Gödel etc.) show that general automation in program proofs and theorem proving is impossible. This does not prevent partial yet industrially relevant solutions.

SAT/SMT solving

A central ingredient in many methods for symbolic and concolic executions, for finding inductive invariants, and for checking their inductiveness, is _satisfiability modulo theory_ (SMT). SMT is based on Boolean satisfiability testing (SAT), that is, checking whether a propositional formula has a solution. There exist algorithms for solving SAT and many cases of SMT, but the issue here is computational complexity: SAT is a hard problem.

Prerequisites

Knowledge in a programming language (Python, C++, OCaml…) to implement the project. Fluency with programming in general. Knowledge of first-order logic and basic mathematics.

Targeted skills

Understanding the main ideas in SAT/SMT algorithmics.

Teacher

David Monniaux