Formal Methods -- (2010-2011)

This page contains the material relevant to Formal Methods (academic Year: 2010-2011 -- Second 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, POS Building, Room 2.03. Appointments have to be previously arranged via e-mail.

TEACHING ASSISTANT: Dr. Alessandro Artale

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. LTL Automata Based Model Checking

9. 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 Specifications

5.Hanoi et al.

6. Asynchronous Mutual Exclusion

7. Exercise: Asynchronous Inverter

8. Past Exam Papers 1 and 2

SUCCESS STORIES

1. CMU Paper

2. NASA

3. IBM

4. TranSwitch

5. Praxis - Lockheed

PROJECTS

The following is the list of NuSMV projects. Choose the "cannibal" problem and also another at your own choice. Submit the NuSMV code by email no later than Friday the 1st of July 2011.

1. Cannibals and Missionaries

2. The Elevator

3. Mutual Exclusion Protocol

4. Queen Game