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) Firstorder 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) Nonterminaison 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) PSPACEcompleteness 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 EXPTIMEcomplete 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 
