Formal verification

Fall semester 2005/2006 (previous year: 2004/2005)
Instructor: Marius Minea
marius@cs.utt.ro

Course information

Lectures: Thu 17-19, A315
Project: Thus 19-20, B528
Office hours: on request

Evaluation:
Projects and homeworks: 50.
Midterm: 25%
Final exam: 25%
Results

Lecture notes

1. Introduction to Formal Methods PDF, 1:1 1:6, for printing
2. Model Checking Basics PDF, 1:1 1:6, for printing
3. Symbolic Model Checking PDF, 1:1 1:6, for printing
4. Partial Order Reduction. Model Checking with Automata PDF, 1:1 1:6, for printing
5. Verification of Timed Systems PDF, 1:1 1:6, for printing
6. Elements of Mathematical Logic PDF, 1:1 1:6, for printing
7. Comparing Models. Abstraction. Compositional Reasoning PDF, 1:1 1:6, for printing
8. Program semantics, analysis and verification PDF, 1:1 1:6, for printing
9. Static analysis PDF, 1:1 1:6, for printing
   Optional (makeup lecture): Program verification in practice PDF, 1:1 1:6, for printing
10. Abstract interpretation: widening and narrowing PDF, 1:1 (slides by Doug Gregor, RPI -- see pages 6 through 18)
11. Verification of security protocols PDF, 1:1 1:6, for printing

Projects and homeworks

Project 2
Modeling and verification of a fabrication system using UPPAAL
Handed out: Nov. 10. Due: Dec. 8