CISC422/853: Formal Methods in Software Engineering: Computer-aided Verification (Winter 2009) Detailed course content [Home] [Content] [Schedule] [Readings] [Assignments] [Tools] [Projects] [Messages]

Topics to be covered

1. Introduction, motivation and overview [Hol04 (Chp1)]
   1. The intricacies of parallel programming
2. Modeling the behaviour of systems [Hol04 (Chp6-7)]
   1. Finite state automata
   2. Non-determinism
   3. synchronous and asynchronous composition
   4. Extensions (e.g., StateCharts, CCS, Petri Nets)
3. Intro to BIR and Bogor [Bogor web pages]
4. Intro to Promela and Spin [Hol04 (Chp3,Chp7,App A)] [Spin web pages]
5. Model Checking, Part 1 [Hol04 (Chp8)]
   1. Computation trees
   2. Random exploration
   3. Guided exploration
   4. Exhaustive exploration
6. Expressing properties of the behaviour of systems [Hol04 (Chp4,Chp6) and course notes]
   1. Intro to formal specification
   2. Assertions
   3. Invariants
   4. Safety and liveness properties
   5. Regular expressions, Buechi-automata, and never-claims
   6. Linear Temporal Logic (LTL)
   7. Computation Tree Logic (CTL) [course notes]
   8. Specification patterns
7. Model Checking, Part 2 [Hol04 (Chp8) and course notes]
   1. Checking safety properties
   2. Checking liveness properties using Buechi automata
   3. Checking LTL properties
   4. CTL Model Checking [course notes]
8. Optimizations [Hol04 (Chp8-9)]
   1. Statement merging, state compression, on the fly model checking [Hol04 (Chp8-9)]
   2. Stateless search and Partial order reduction [Hol04 (Chp9)]
   3. Data abstraction
   4. Static analysis and slicing
   5. Predicate abstraction (time permitting)
9. The Software Model Checking Landscape
   1. Automated model extraction
   2. Counter-example driven abstraction refinement
   3. Modified execution environments