Preliminary List of Topics
Policy, process & methodology
- Formalism and anti-formalism
- Risks, catastrophes and cost-benefit analysis
- The world beyond interfaces
Logical foundations
- First order logic
- Relational calculus
- Modal logics
Analysis mechanisms
- Reduction to SAT
- Symbolic model checking
Examples
- Electronic voting
- Role-based access control
- Colour management
- File synchronization
- Radiotherapy software
- Generic naming schemes
- Undo/redo mechanisms
Languages and tools
- Alloy, Z, B, Larch, SPIN, SMV, ESC, JML
Patterns of modelling and analysis
- States, invariants and operations
- Incremental state, operation splitting and views
- Declarative spec, non-determinism, frame conditions and vacuity
- Patterns for analyzing object-oriented programs
- Temporal properties: safety and liveness, deadlock and races
- Guarded commands
- Hoare triples and weakest preconditions
- Refinement, abstraction and abstract interpretation
Readings
Students of the class will be given access to a private website containing pdf readings for the course.