CVFP Conception et vérification formelle de programmes 
Software design and verification

Magistère informatique et télécommunications - ENS Rennes - Année 2013/2014


Cours : François Schwarzentruber
Travaux dirigés : Martin Bodin

You may also find some materials on the CVFP website of Martin.


12 september 2013 Presentation of the course
- Software failures
- Why do we have failure and may be the solutions? (brainstorming)
- What do you learn in this course: design, model checking and decidable theories for proofs of algorithms
Part 1: Software design
Chapter 1. Software analysis

I) Requirements analysis
1) UML use case diagrams
2) UML sequence diagrams
II) Analysis of the domain
1) First-order logic
2) UML object diagrams
3) UML class diagrams
4) Comparison between FO and UML
UML pictionary game (pdf + source)
17 september 2013 Chapter 2. Object design
I) Symptoms of a rotting system Slides
II) Good principles
1) Principles of object oriented class design
2) Principles of package architecture
III). Design patterns Slides
1) Creation
2) Structural
3) Behaviour
24 september 2013 Part 2: Introduction to modal logic
Chapter 1: modal logic: a decidable fragment of first order logic
I) Two good properties: axiomatization and finite model property
II) Syntax of modal logic K
III) Semantics
IV) Translation into first order logic
V) Axiomatization
VI) Finite model property: filtration
1 october 2013 Chapter 2: Expressivity
I) Recall of expressivity of first order logic
II) Expressivity of modal logic
a) Bounded morphism
b) Bissimulations
c) Bissimulations as a characterisation
d) Bissimulation and first order logic

- History of modal logic
- Few notes about completeness proof

About projects
Monday (!) 7 october 2013 Part 3: Model checking
Chapter 1: Introduction to model checking
I) Discussions
- tests
- definition of model checking
- Rice's theorem
II) From programs to Kripke structures
1) Program graph
2) Kripke structures
3) Concurrency
II) The CTL* language for properties
- syntax
- properties (safety, liveness, fairness)
- semantics
- decision problems
- LTL, CTL fragments

T 8 oct: TP1 Spin

M 14 oct: TD4 (bis)

T 15 oct: TP2 Coq

Monday (!) 21 october 2013 Chapter 2: decision procedures
I) Introduction
- model checking VS satisfiability problem

I) Model checking
1) Model checking in CTL
a) Building the algorithm
b) Example
2) Model checking in LTL
Reduction to SAT of LTL

II) Satisfiability problem for K
1) Tableau rules
2) Example
3) Algorithm

22 october 2013
4) Proof of terminaison, complexity (in polynomial space) and correction of the algorithm)

III) Satisfiability problem for LTL
1) Tableau rules
2) Non-terminaison and fullfilment problem
5 november 2013 Chapter 3: Complexity theory and temporal logics
I) Alternating Turing machine
a) Definition
b) Computation
c) Acceptation of a language
d) A plethora of complexity classes
a) Tilings of squares
b) SAT
c) Fragment of K and LTL
a) Corridor tiling problem
b) PSPACE-completeness of satisfiability and model checking of LTL
c) PSPACE as a game: QBF

12 november 2013
d) Savitch's theorem
f) Modal logic K
a) As a game: EXPTIME = ASPACE
b) An EXPTIME-complete tiling problem
c) SAT of CTL

19 november 2013 Chapter 4: expressivity
I) LTL is better than CTL
II) CTL is better than LTL
Partial order reduction?

26 november 2013 Talk (68NQRT talks)

Joel Ouaknine, Oxford University

Decision Problems for Linear Recurrence Sequences

Linear recurrence sequences (such as the Fibonacci numbers) permeate a vast number of areas of mathematics and computer science (in particular: program termination and probabilistic verification), and also have many applications in other fields such as economics, theoretical biology, and statistical physics. In this talk, I will focus on three fundamental decision problems for linear recurrence sequences, namely the Skolem Problem (does the sequence have a zero?), the Positivity Problem (are all terms of the sequence positive?), and the Ultimate Positivity Problem (are all but finitely many terms of the sequence positive?). This is joint work with James Worrell.

3 december 2013 Chapter 5: Abstraction
I) (Bi)simulation
1) Bisimulation (equivalence with CTL* and CTL)
2) Simulation
3) Simulation equivalence (with ECTL*, ACTL*, ECTL, ACTL)
II) Quotient
1) Definition
2) Simulation
3) Bisimulation (+ algo for computing M/bis)

(Bonus: Proposition Dynamic Logic : cancelled)
Monday 9 december, 2pm KERMESSE
Presentation of the projects


Modal logic. Blackburn, P. and De Rijke, M. and Venema, Y. 2002
Dynamic logic. Harel, D. and Kozen, D. and Tiuryn, J. The MIT press, 2000

Principles of model checking. Baier, C. and Katoen, J.P. and ebrary, Inc. The MIT press, 2008
Vérification de logiciels: Techniques et outils du model-checking. P Schnoebelen, B Bérard, M Bidoit, F Laroussinie. 1999

Sipser, M. (2006). Introduction to the Theory of Computation (Vol. 2). Boston: Thomson Course Technology.


Pedagogic tableau provers for modal logic

Lotrec, a generic prover for modal logics
LotrecScheme, a generic prover based on the idea of Lotrec
Mettel2, another generic prover

Prover in description logic

Fact a prover for description logic
Fact++, the same prover in C++
A comprehensive list of provers for description logic 

Model checkers

Spin, model checker for LTL
Java Path Finder, model checker applied to JAVA code
NuSMV, model checker for CTL

SLAM, model checker for interfaces
BLAST, model checker for C programs