|
|
CMSC 630 --- Foundations of Software Verification Spring 2010
|
Below is a list of lecture topics by date, as well as significant milestones throughout the semester. The lecture list is provisional and subject to change (last modified: 1/15/2010).
|
Tu 01/26 |
Course intro; review of propositional calculus |
|
Th 01/28 |
Review of predicate calculus |
|
Tu 02/02 |
Hoare logic for sequential programs: semantics |
|
Th 02/04 |
Hoare: proof rules, outlines; soundness and completeness |
|
Tu 02/09 |
Owicki-Gries logic and concurrency |
|
Th 02/11 |
Owicki-Gries: soundness and completeness |
|
Tu 02/16 |
Temporal logic and Kripke structures |
|
Th 02/18 |
Linear vs. branching time temporal logic |
|
Tu 02/23 |
|
|
Th 02/25 |
|
|
Tu 03/02 |
|
|
Th 03/04 |
(Project proposal due) |
|
Tu 03/09 |
|
|
Th 03/11 |
MIDTERM |
|
Tu 03/16 |
SPRING BREAK |
|
Th 03/18 |
SPRING BREAK |
|
Tu 03/23 |
Buechi automata and LTL model checking |
|
Th 03/25 |
Buechi automata and LTL model checking (cont.) |
|
Tu 03/30 |
Process algebra and a Calculus of Communication Systems |
|
Th 04/01 |
Bismulations |
|
Tu 04/06 |
Equivalences for |
|
Th 04/08 |
(Project status report due) Logical characterizations of equivalences |
|
Tu 04/13 |
Proof systems for equivalences |
|
Th 04/15 |
Proof systems (cont.) |
|
Tu 04/20 |
Algorithms for bisimulation equivalence |
|
Th 04/22 |
Computing observational equivalence |
|
Tu 04/27 |
Simulation, testing and refinement relations |
|
Th 04/29 |
Review |
|
Tu 05/04 |
Project presentations |
|
Th 05/06 |
Project presentations |
|
Tu 05/11 |
Project presentations |
|
Fr 05/14 |
FINAL (8:00 am – 10:00 am) |