Description: UMD_logo

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 CTL

W 02/25

CTL model checking

M 03/02

CTL model checking (cont.)

W 03/04

(Project proposal due)

CTL model checking (cont.)

M 03/09

Buechi automata; review

W 03/11


M 03/16


W 03/18


M 03/23

Buechi automata and LTL model checking

W 03/25

Process algebra and a Calculus of Communication Systems

M 03/30


W 04/01

Equivalences for CCS

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)