DESCRIPTION

As the complexity of computer systems grows, their reliability and security can no longer be sufficiently controlled by the traditional approaches of testing 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.

More info here.