06-02489 Automatic Verification

Dan Ghica,  Manfred Kerber 10 credits in Semester 2

Recommended Reading

Title Author(s) Publisher Comments
Systems and Software Verification - Model-Checking Techniques and Tools B. Berard et al. Springer, 2001 Library QA 76.76.V47 S
Logic in Computer Science: Modelling and reasoning about systems Michael R A Huth and Mark D Ryan Cambridge University Press 2000 Module Section School Library
Model Checking Edmund M. Clarke, Orna Grumberg, and Doron A. Peled MIT Press 1999 Library QA 76.76.V47 C
SAT-based Bounded and Unbounded Model Checking Edmund M. Clarke Tutorial FLOC 2006 Further reading
Simultaneous SAT-Based Model Checking of Safety Properties Z. Kahsidashvili, A. Nadel, A. Palti, Z. Hanna Haifa Verification Conf. 2005 Further reading
Computational Tree Logic and Model Checking F. Raimondi Tutorial Further reading
Lecture 0: Computational Tree Logics Edmund M. Clarke CMU lecture Further reading
An Analysis of SAT-based Model Checking Techniques in an Industrial Environment Nina Amla et al. conference paper CHARME 2005 Further reading
Chaff: Engineering an Efficient SAT Solver Matthew W. Moskewicz et al. System description Further reading
Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning Alessandro Armando and Luca Compagna conference paper: FORTE 2002 Formal Techniques for Networked and Distributed Systems Further reading
Planning as Model Checking Paolo Traverso Tutorial Further reading
Fatal Dose Barbara Wade Rose Description on software related radiation accidents Motivation
Ariane 5 accident J. L. Lions et al. Description on software related rocket explosion Motivation
Warsaw plane accident Peter B. Ladkin and Aircraft Accident Investigation Description on software related aeroplane accident Motivation
Pentium bug Thomas R. Nicely Description of detection of Pentium hardware bug Motivation
Mars Climate Orbiter NASA Description of detection of Loss of Mars Climate Orbiter Motivation

Detailed Syllabus and Relevant Links

Week Lectures Handouts (internal access only)
1Motivation, Hoare Calclusus h1.pdf
2Finite State Machines h2.pdf
7CTL*, CTL, LTL, ETL h3.pdf
8Model Checking in CTL h4.pdf
10LTL to Prop, BDD, SAT solving h5.pdf


Maintained by: Manfred Kerber, School of Computer Science, University of Birmingham
Last update: 14.3.2008.
The URL of this page is   http://www.cs.bham.ac.uk/~mmk/Teaching/Verification/index.html.