|
|
CMSC 630 --- Foundations of Software Verification Spring 2015
|
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: 01/26/2015).
|
M 01/26 |
Course intro; propositional calculus |
|
W 01/28 |
The sequent calculus: proofs in the propositional calculus |
|
M 02/02 |
Predicate calculus |
|
W 02/04 |
Hoare logic for sequential programs: semantics |
|
M 02/09 |
Hoare logic: proof rules, outlines, loop invariants, weakest preconditions |
|
W 02/11 |
Hoare logic: soundness and relative completeness; Owicki-Gries logic and concurrency |
|
M 02/16 |
Owicki-Gries: soundness and completeness |
|
W 02/18 |
Temporal logic and Kripke structures |
|
M 02/23 |
Linear vs. branching time temporal logic; CTL* and |
|
W 02/25 |
|
|
M 03/02 |
|
|
W 03/04 |
(Project proposal due) |
|
M 03/09 |
Buechi automata; review |
|
W 03/11 |
MIDTERM |
|
M 03/16 |
SPRING BREAK |
|
W 03/18 |
SPRING BREAK |
|
M 03/23 |
Buechi automata
and LTL model checking |
|
W 03/25 |
Process algebra and a Calculus of Communication Systems |
|
M 03/30 |
Bisimulations |
|
W 04/01 |
Equivalences for |
|
M 04/06 |
Logical characterizations of equivalences |
|
W 04/08 |
(Project status report due) Proof systems for equivalences |
|
M 04/13 |
Proof systems (cont.) |
|
W 04/15 |
Algorithms for bisimulation equivalence |
|
M 04/20 |
Computing observational equivalence |
|
W 04/22 |
Simulation, testing and refinement relations |
|
M 04/27 |
Simulation, testing and refinement relations (cont.) |
|
W 04/29 |
Project presentations |
|
M 05/04 |
Project presentations |
|
W 05/06 |
Project presentations |
|
M 05/11 |
Project presentations |
|
Sa 05/16 |
FINAL (1:30 pm – 3:30 pm) |