ALaRI Hang Glider

Search form

Education and Innovation in Embedded Systems Design

USI Università della Svizzera italiana, USI Faculty of Informatics, Advanced Learning and Research Institute USI Università della Svizzera italiana USI Faculty of Informatics USI Advanced Learning and Research Institute

Validation and Verification II

Professor Sharygina Natasha
Course program MAS
Year 1
Semester Spring
Category Elective
Academic year 2013/2014

Course type: Lecture
Value in ECTS: 3

Academic year 2013/2014 - 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.