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
- describe the basic ideas behind a range of modern tools and techniques in the area of software verification
- apply such tools to detect errors in small-scale programs
- evaluate the tools according to expressive power, domain of applicability, degree of automation, efficiency, soundness, and completeness
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.