The course consists of two parts. The first part is taught by Florence Maraninchi. Please see the course homepage for more details. The second part is taught by me.

The second part of the course gives an introduction to a verification technique called model checking. We will consider the two temporal logics Computation Tree Logic (CTL) and Linear temporal logic (LTL) to express desired properties. LTL and CTL are the core of industrial logics like System Verilog Assertions (SVA) or Property Specification Language (PSL). Given a system and a desired property of the system (aka the specification), we will study algorithms that check if the system satisfies the property.

The second part of the course is structured as follows:- Wednesday Nov 23 (7): Examples of systems and properties that can be verified by model checking, translation of (simple subset of) Verilog to transition graphs, definition of Computation Tree Logic (CTL).
- Wednesday Nov 30 (8): CTL model checking based on fixpoint computation
- Wednesday Dec 7 (9): Symbolic Model Checking and Binary Decision Diagrams
- Wednesday Dec 14 (10): CTL model checking with Fairness, Bisimulation, Simulation Relation, and Linear-Time Logic (LTL)
- Wednesday Jan 4 (11): LTL Model Checking

- Slides for lecture on 23/11/2011:
(1) Introduction, Examples, CTL Syntax and Semantics,

Examples: counter.v counter4Bit.v cell.v arbiter.v arbiter.ctl kripke.v kripke.ctl puzzel.v puzzel.ctl puzzel_2.v puzzel_2.ctl - Material for exercises on 23/11/2011:
How to get started with VIS on ensisun,
Assignment
(mutex.v,
elevator.v)

You can get VIS for your own computer here.

Solutions: Kripke structure of mutex.v, CTL formulas for mutex.v, Verilog Model of elevator, CTL Formulas for elevator model - Slides for lecture on 30/11/2011: (2) CTL Model Checking
- Material for exercises on 30/11/2011: Assignment, Solutions
- Slides for lecture on 7/12/2011: (3a) Symbolic Model Checking, (3b) BDDs (thanks to Daniel Kroening for the slides)
- Material for exercises on 7/12/2011: Assignment, miniBDD source code, Solutions
- Slides for lecture on 14/12/2011: (4) Fairness constraints, (5) Bisimluation, Simulation Relation, and Linear Temporal Logic (LTL)
- Material for exercises on 14/12/2011:
Assignment

Dining philosophers: dining-v1.v, dining-v2.v

Example on how to using fairness constraints in VIS, Solutions - Slides for lecture on 04/01/2012: (6) LTL Model Checking
- Material for exercises on 04/01/2012: GOAL - a tool for manupulating Büchi automata, Assignment, Solutions

- What can binary decision diagrams (BDDs) be used for? by R. Bryant
- Lectures on Software Reliability by D. Peled
- Course on Logic and Automta Theory by R. Iosif and B. Jobstmann
- Property Description Logics: SystemVerilog Assertions (SVA) (SystemVerilog Standard, Section 17) , Property Specification Language (PSL), for more details see the standardization organization Accellera or SystemVerilog Assertion Committee

- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, 1992.
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety, 1995.
- E. Clarke, O. Grumberg, and D. Peled, Model Checking, 2000.
- C. Baier and J.-P. Katoen, Principles of Model Checking, 2008.
- B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci and Ph. Schnoebelen. Model-Checking Techniques and Tools, Springer, 2001. French version: Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie and A. Petit. Vérification de logiciels : techniques et outils du model-checking. Vuibert, 1999.

- Cadence (Assertion-based Verification)
- Esterel Technologies (SCADE Tool, in particular, the Design Verifier)
- IBM (Sixth Sense and RuleBase)
- Jasper Design Automation (Jasper Gold)
- Mentor Graphics (Questa Formal Verification)
- Prover Technologies
- Synopsys (VCS)
- The MathWorks/Polyspace