Computer Aided Verification

Professor: Natasha Sharygina
Assistant: Simone Fulvio Rollini

Course type: Lecture
Value in ECTS: 6
Bibliographic references available on the University Library website

Academic year 2012/2013 - Spring semester – not offered

Contents
As the complexity of computer systems grows, their reliability and security can no longer be sufficiently controlled by the traditional approaches of test-ing and simulation. Model checking and related computer aided verification techniques are practical alternatives to simulation for debugging complex systems. These methods allow the designer to verify that a mathematical model of a system satisfies the system’s formalised requirements, or to systematically seek for cases where it fails to do so. This approach has been most effective in the analysis of hardware designs, and is an integral part of the design cycle in companies like Intel, IBM, and Cadence. Much recent research has focused on applying similar techniques to improve the reliability of systems software. The course introduces the theory and practice of formal methods for the design and analysis of concurrent and embedded systems. The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity. Topics include: Models and semantics of reactive systems: formal models for concurrent systems with software and hardware components; Verification algorithms: temporal logic by model checking, theory of omega automata, equivalences and refinement; Verification techniques: symbolic model checking, on-the-fly model checking, state space reduction methods, compositional reasoning, and automatic abstraction. Students will experiment with checking the system correctness by writing formal proofs manually and by applying fully automated verification tools.