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