Course type: Lecture
Value in ECTS: 3

Academic year 2014/2015 - Spring semester

Overview of the course:

In the recent decade, the advances in symbolic modeling and automated state space reduction enabled formal verification by model checking to become a mainstream technology in the automated validation of embedded systems and integrated circuits designs. This course introduces the students to advances in symbolic verification using Boolean Satisfiability (SAT) engines and presents methods for automated abstraction that reduce the intrinsic complexity of model checking. The course will proceed by discussing how to model systems symbolically while retaining full semantics of the original designs and how to exploit the efficiency of SAT solvers for checking correctness of the system models, then it present automated abstraction techniques such as predicate abstraction, counterexample-abstraction refinement (known as CEGAR) and interpolation essential for efficient analysis of complex systems. We will discuss how all these techniques can be effectively combined for word-level reasoning to enable register-transfer level analysis of integrated circuits. The course will conclude with a lab using the VCEGAR model checker, implementing symbolic modeling and the CEGAR framework for Verilog designs.