CMSC 630 --- Theory of Programming Languages

Spring 2007

Tentative Course Schedule

Th        01/25

Course intro; review of propositional calculus

Tu        01/30

Review of predicate calculus; verification frameworks

Th        02/01

Hoare’s logic for sequential programs

Tu        02/06

Owicki-Gries logic for concurrent programs

Th        02/08

Owicki-Gries (cont.)

Tu        02/13

Temporal logic verification:  Kripke structures

Th        02/15

Syntax and semantics of temporal logic

Tu        02/20

A proof technique for temporal logic

Th        02/22

Model-checking via Buechi automata

Tu        02/27

Model checking (cont.)

Th        03/01

Linear vs. branching time temporal logic

Tu        03/06

CTL and fixed points

Th        03/08

(Project proposal due)

CTL model checking as fixed point iteration

Tu        03/13

Efficient CTL model checking

Th        03/15

MIDTERM

Tu        03/20

SPRING BREAK

Th        03/22

SPRING BREAK

Tu        03/27

Symbolic model checking using binary decision diagrams

Th        03/29

Model checking via Boolean equation solving

Tu        04/03

Real-time model checking

Th        04/05

Real-time model checking (cont.)

Tu        04/10

Process algebra and the Calculus of Communication Systems

Th        04/12

(Project status report due)

Modeling event-driven systems in process algebra

Tu        04/17

Labeled transition systems and bisimulation equivalences

Th        04/19

Proving bisimulation equivalence

Tu        04/24

Algorithms for bisimulation equivalence

Th        04/26

Computing observational equivalence

Tu        05/01

Simulation, testing and other semantic refinement relations

Th        05/03

Computing diagnostic tests

Tu        05/08

Project reports

Th        05/10

Project reports

W        05/16

FINAL (10:30am—12:30pm)