Computer Aided Verification
People
Course director
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.
Specialised course of the research areas
Software Engineering and Theory and
Algorithms
Education
- Master of Science in Informatics, Core course, Lecture, 1st year