Formal Methods -- (2009-2010)

This page contains the material relevant to Formal Methods (academic Year: 2009-2010 -- First Semester) module including lecture handouts and practical material. All enquiries regarding the module should be addressed to Alessandro Artale.

This is the Course Presentation Form with the syllabus of the course.

OFFICE HOURS: Tuesday, 15:00-17:00, Faculty of CS, Via della Mostra, 4, first floor. Appointments have to be previously arranged via e-mail.

TEACHING ASSISTANT: Prof. Enrico Franconi

LECTURES

1. Introduction to FM

2. Modeling Systems

3. Linear Temporal Logic -- LTL

4. Computation Tree Logic -- CTL

5.1 CTL Model Checking

5.2 CTL Model Checking with Fairness Constraints

6. Binary Decision Diagrams (BDD's)

7. CTL Symbolic Model Checking

8. Model Checking Vs. Proof Theory

USEFUL MATERIAL

2. Propositional Logic (Enrico Franconi)

2.1 Propositional Logic -- Reasoning (Enrico Franconi)

3. First Order Logic (Enrico Franconi)

3.1 First Order Logic -- Reasoning (Enrico Franconi)

4. Introductory Lecture from E. Clarke (Edmund Clarke)

TUTORIALS And LABS

1. The NuSMV Model Checker (download here)

2. Exercise: Short

2.1. Exercise: Counter

3. Exercise: Mutual Exclusion

3.1 Exercise: Mutual Exclusion (source code)

3.2 Exercise: Mutual Exclusion (solution)

4. Exercise: Tic-Tac-Toe

4.1 Tic-Tac-Toe Solution

5.Hanoi et al.

6. Asynchronous Mutual Exclusion

7. Exercise: Asynchronous Inverter

8. Past Exam Paper

SUCCESS STORIES

1. CMU Paper

2. NASA

3. IBM

4. TranSwitch

5. Praxis - Lockheed

PROJECTS

The following is the list of NuSMV projects. Choose one project and submit the NuSMV code by email no later than the 12th of February 2010.

1. Cannibals and Missionaries

2. The Elevator

3. Mutual Exclusion Protocol