Teachers:
Dr. Suzana Andova HG 7.23, tel: 5089, s.andova@tue.nl
2if25 is an introduction to
formalization and the then possible (partial) automation of verification. It
both provides an overview of what is available for
those that take this as the only course in that direction, as well as provide a
basis for more advanced or specialized lectures.
During the course we shall discuss what formalization and automation is about,
what can and cannot be done, completeness, decidability, etc.
Two 2hour lectures plus two 2hour exercise sessions on each topic are the
basis for the course. Material is handouts that will also appear on studyweb
and, additionally, copies of papers. Successful participation in the exercise
sessions provides one bonuspoint towards the exam result.
Outline of contents of 2if25
A simpel formal model for system behavior: Transition system.
I. The finite case: propositional logics
1. Specification languages to specify properties of systems.
Propositional logic.
Propositional modal logic.
Propositional linear time logic: LTL.
Propositional branching time logic, limited version: computation tree logic, CTL.
Propositional branching time logic, full version: CTL*.
Propositional modal mcalculus.
2. Model checking formulas in the above propositional logics against finite transition systems, i.e., models of system behavior.
The labeling approach for modal logic and CTL.
The intersection of automata approach for LTL.
The combination of the above two for CTL*.
The recursive algorithm for modal mcalculus.
II. The potentially infinite case: first order logics
1. Specification languages to specify properties of systems.
Hoare logic for programming languages.
First order LTL for parallel components.
2. Theorem proving.
Automated theorem proving for first order logic.
Sequent calculus for automated proving of first order formula (PVS).
Sequent calculus for automated proving first order formulas over of first order axiomatizations of programs (PVS).
Sequent calculus for automated proving of Hoare logic formulas (Cocktail, PVS, ESC/Java?, Spec#?).
Automated theorem proving for first order LTL.
i. Proof system for (automating) proving of first order LTL formulas (Manna/Pnueli).
ii. Proof system for (automating) proving of first order LTL formulas over first order LTL descriptions of programs (Manna/Pnueli).
iii. Proof system for (automating) proving of first order LTL formulas over programs (STEP, Manna).
Course planning:
date 
topics 
lecture notes 
exercises 

lecture 1 
Introduction 
No exercise class on Wednesday August 27 

lecture 2 
Modal logic, LTL  
lecture 3 
CTL* and CTL  lecture notes 3  
lecture 4 
mu calculus 
distributed papers 

lecture 5 
CTL model checking  
lecture 6 
LTL model checking  
14Oct2008  All previous topics  First test 
First Test No instruction on October 15 
lecture 7  SMV symbolic model checker  material and examples  
lecture 8  CTL* and mucalculus model checking  distributed material  Exercises 
lecture 9 
Program verification 
Hoare triples, proof rules 
distributed material  Exercises Program verification 
lecture 10  Theorem proving  distributed material  Exercises Theorem proving 
lecture 11  Cocktail tool  Michael Franssen  lecture slides 
Download for the instructions Cocktail tool for 
lecture 12 
Program verification  MannaPnueli logic 
distributed material (Chapter 0 from [2]) 
Exercises  Problems 0.10.4 from [2] pg.6670 
lecture 13 
Program verification 
Invariants 
distributed material (Chapter 1 from [2]) 
Exercises and Problems Chapter 1 from [2] 
lecture 14 
Program verification Response 
distributed material  Second test  Hints for solutions 
Lecture 12: From Chapter 0 of [2] distributed during the lecture 12 the following parts might be excluded:
send and receive statements, pg. 1617, pg. 3341.
Lecture 13: From distributed material covering the lecture 13, Chapter 1 of [2],
the following parts are included: pg. 81101 and pg. 120122.
Lecture 14: From the distributed material from [3] the following parts are
included: pg. 112 and pg.1922 and pg. 147159.
Copies of the material from lectures can be found on the table at front of HG. 7.23.
The lectures are based mainly on
[1] D. Peled, Software Reliability Methods, Springer 2001, ISBN 0387951067
[2] Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems: Safety, Springer 1995.
[3] http://theory.stanford.edu/~zm/tvors3.html
Download The Cadence SMV Model Checker (not SMV from Carnegie Mellon university!) for the instructions on Wed. 22102008.
Additional Information:
Instruction: check the OWI web site http://w3.tue.nl/nl/diensten/stu/
The exam: written examination; use of books, handouts etc. allowed.