Program Testing and Verification - WMM9MO73

Goal(s)

Understanding the various approaches used for testing and proving code, their strength and limitations.

Content(s)

Testing is a well-known approach for ascertaining if a program works correctly: one runs the program, or parts thereof, on examples (handwritten 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 input values 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.

Fluency with programming in general.
C language.
Knowledge of first-order logic and basic mathematics.