College Formele Methoden 2008-2009 (2IF25)


Teachers:


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 2-hour lectures plus two 2-hour exercise sessions on each topic are the basis for the course. Material is handouts that will also appear on study-web
and, additionally, copies of papers. Successful participation in the exercise sessions provides one bonus-point towards the exam result.
 

Outline of contents of 2if25

I. The finite case: propositional logics

1. Specification languages to specify properties of systems.

  1. Propositional logic.

  2. Propositional modal logic.

  3. Propositional linear time logic: LTL.

  4. Propositional branching time logic, limited version: computation tree logic, CTL.

  5. Propositional branching time logic, full version: CTL*.

  6. Propositional modal m-calculus.

2. Model checking formulas in the above propositional logics against finite transition systems, i.e., models of system behavior.

  1. The labeling approach for modal logic and CTL.

  2. The intersection of automata approach for LTL.

  3. The combination of the above two for CTL*.

  4. The recursive algorithm for modal m-calculus.

II. The potentially infinite case: first order logics

1. Specification languages to specify properties of systems.

  1. Hoare logic for programming languages.

  2. First order LTL for parallel components.

2. Theorem proving.

  1. Automated theorem proving for first order logic.

     

    1. Sequent calculus for automated proving of first order formula (PVS).

    2. Sequent calculus for automated proving first order formulas over of first order axiomatizations of programs (PVS).

    3. Sequent calculus for automated proving of Hoare logic formulas (Cocktail, PVS, ESC/Java?, Spec#?).

     

  2. 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
to Formal Methods

lecture notes 1

 

No exercise class on Wednesday August 27

lecture 2
 

Modal logic, LTL

lecture notes 2

Exercises Transition systems, Modal Logic and LTL

Solutions Exercise 1  and   figures

lecture 3
 

CTL* and CTL    lecture notes 3

Exercises CTL and CTL*

Solutions Exercise 2 and figures

lecture 4
 

mu calculus

distributed papers

Exercises mu calculus

Solutions

lecture 5
 

CTL model checking

lecture notes 5

Exercises Model checking CTL

Solutions

lecture 6
 

LTL model checking

lecture notes 6

Exercises Model checking LTL

Solutions

14-Oct-2008 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 mu-calculus model checking  distributed material Exercises

Solutions

lecture 9 Program verification -

Hoare triples, proof rules

distributed material Exercises Program verification

Solutions

lecture 10 Theorem proving distributed material Exercises Theorem proving

Solutions

lecture 11 Cocktail tool - Michael Franssen lecture slides

Download for the instructions Cocktail tool for

Linux

Windows

Mac

lecture 12 Program verification -

Manna-Pnueli logic

distributed material

(Chapter 0 from [2])

Exercises - Problems 0.1-0.4 from [2] pg.66-70

Solutions

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. 16-17, pg. 33-41.

 

Lecture 13: From distributed material covering the lecture 13, Chapter 1 of [2], the following parts are included: pg. 81-101 and pg. 120-122.
 
Lecture 14: From the distributed material from [3] the following parts are included: pg. 1-12 and pg.19-22 and pg. 147-159.

 

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 0-387-95106-7

[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. 22-10-2008.


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.