Program verification

It has become obvious that ad-hoc testing is not a realible and scalable approach to safeguard against fatal and costly errors. This course will show you more advanced techniques to verify software against its specification. Topics handled include automated test generation, model checking, and theorem proving. Automated test generation is a cheap and fast way to discover errors. For critical software, the coverage of automated test is however still inferior. Model checking is a more sophisticated technique. It has complete coverage (with respect to the specification). It does have its limitation. It has to deal with state explosion, which can be very bad in, for example, concurrent programs. A more fundamental limitation is that model checking only works on programs with finite state space. To handle programs with infinite state space we have to turn to a more generic approach called theorem proving. Modern theorem proving tools are usually based on very expressive logics which make them very versatile. Although in principle theorem proving is not an automated approach, modern tools do come with powerful automation libraries. Because of their versatility they potentially have many applications. In addition to discussing techniques we will also show a range of tools, e.g. HOL, SPIN, Jtest, SLAM, Isabelle ... The course includes lab sessions and assignments to give you first hand experience with some of those tools.

Course outline:

1. Modelling in Higher Order Logic.
2. Principles of theorem proving in Higher Order Logic
3. Proof scripting
4. Model checking, including a case study
5. Automated testing tools
6. Automated error finding via abstraction
7. Embedding
8. Selected topics (e.g. verification of security protocols)