Software Verification

[THIS COURSE IS GIVEN NEXT TIME IN 2012!]

Aims and Contents

Detection of intricate programming errors may require application of advanced program analysis and verification techniques for modeling resources, temporal properties, datatype invariants, and security properties. These techniques range from light-weight simulations over medium-weight static analysis or model checking to heavy-weight theorem proving and axiomatic semantics. This course will investigate recent advances in the area, in particular connections between the various approaches.

The student will become able to

Additionally, the student will be trained in reading and presenting scientific articles.

In the course, we shall study and evaluate concrete software verification tools and techniques by reading and discussing research papers, performing practical experiments with the tools, and writing brief reports that summarize the main ideas.

Prerequisites: Compilation (dOvs), Computability and Logic (dBerLog) and Static Analysis.

Lecturer: Anders Møller <amoeller@cs.au.dk>

Literature: Selected research papers.

Compulsory program: Group presentations.