| 12 september 2013 | Presentation of the course - Software failures
Part 1: Software
design- 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 Chapter 1. Software analysis I) Requirements analysis 1) UML use case
diagrams
II) Analysis of the domain2) UML sequence diagrams 1) First-order logic UML pictionary
game (pdf + source)
2) UML object diagrams 3) UML class diagrams 4) Comparison between FO and UML |
TD1 |
| 17 september 2013 | Chapter 2. Object design I) Symptoms of a rotting system Slides II) Good principles 1) Principles of
object oriented class design
III). Design
patterns Slides2) Principles of package architecture 1) Creation
2) Structural 3) Behaviour |
TD2 |
| 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 |
TD3 |
| 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 Bonus: - History of modal logic - Few notes about completeness proof About projects |
TD4 |
| Monday (!) 7 october 2013 | Part 3: Model checking Chapter 1: Introduction to model checking I) Discussions - tests II) From programs to Kripke structures- definition of model checking - Rice's theorem 1) Program graph
II) The CTL* language for properties2) Kripke structures 3) Concurrency
- 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 2) Model checking in LTLb) Example 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
II) NPb) Computation c) Acceptation of a language d) A plethora of complexity classes a) Tilings
of squares III) PSPACEb) 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 IV) EXPTIMEe) AP = PSPACE 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)
II) Quotient2) Simulation 3) Simulation equivalence (with ECTL*, ACTL*, ECTL, ACTL) 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 |
|