CMSC 630 --- Theory of Programming Languages Spring 2007 Course Schedule

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: 2/13/2007). Here is the original schedule.

Th 01/25	Course intro; review of propositional calculus
Tu 01/30	Review of predicate calculus; verification frameworks
Th 02/01	Hoare logic for sequential programs: semantics of programs	Notes
Tu 02/06	Hoare’s logic: semantics of Hoare triples, proof rules
Th 02/08	Hoare logic: proof outlines, soundness and completeness
Tu 02/13	No class due to university closure	Notes; HW #1 out
Th 02/15	Owicki-Gries logic and concurrency
Tu 02/20	Temporal logic verification	Notes; project ideas; HW#1 due
Th 02/22	No class
Tu 02/27	Linear vs. branching time temporal logic	Notes
Th 03/01	CTL* and CTL
Tu 03/06	CTL model checking	Notes; HW #2 out
Th 03/08	(Project proposal due) CTL model checking (cont.)
Tu 03/13	CTL model checking (cont.)	HW #2 due
Th 03/15	MIDTERM
Tu 03/20	SPRING BREAK
Th 03/22	SPRING BREAK
Tu 03/27	CTL model checking (cont.)
Th 03/29	CTL model checking and binary decision diagrams
Tu 04/03	Process algebra and a Calculus of Communication Systems	Notes
Th 04/05	Bismulations
Tu 04/10	Equivalences for CCS
Th 04/12	(Project status report due) Logical characterizations of equivalences	HW #3 out
Tu 04/17	Proof systems for equivalences
Th 04/19	Proof systems (cont.)	HW #3 due
Tu 04/24	Algorithms for bisimulation equivalence
Th 04/26	Review
Tu 05/01	Project report (Wilson)	HW #4 out
Th 05/03	Project report (Friedler)
Tu 05/08	CLASS CANCELED
Th 05/10	Project report (Ackermann, Zazworka)	HW #4 due
W 05/16	FINAL (10:30am—12:30pm)