CS686 Spring 01
Logics of Programs
Course Information

Instructor

Dexter Kozen kozen@cs.cornell.edu 5143 Upson 255-9209 office 257-4579 home

Time and Place

MW 1:15-2:30, Hollister 306.

Office Hours

By appointment.  Please contact Rosemary Adessa, 5147 Upson, 255-9555.

Workload & Grading

Workload will be minimal. Occasional readings as assigned. Optional homework exercises. Final paper, project, or exam at the student's option.

Topics

Floyd/Hoare Logic
Modal Logic
Dynamic Logic
Temporal Logic
Process Logic
Automata on infinite objects
Rabin tree theorem
The modal mu-calculus
Games and alternating automata
Applications to type inference
Set constraints
Kleene algebra and Kleene algebra with tests

Sources

Dynamic Logic by Harel, Kozen, and Tiuryn.  MIT Press, 2000.

K. R. Apt and E.-R. Olderog, Verification of Sequential and Concurrent Programs, Springer-Verlag, 1991.

C. A. R. Hoare. An axiomatic basis for computer programming. Comm. Assoc. Comput. Mach. 12 (1969), 576-580, 583.

M. C. B. Hennessy and G. D. Plotkin. Full abstraction for a simple programming language. In: Proc. Math. Found. Comput. Sci., Springer-Verlag Lect. Notes in Comput. Sci. 74, New York, 1979, 108-120.

W. Thomas. Languages, Automata, and Logic. Manuscript, May 1996.

M. Vardi, Alternating automata and program verification.

R. Kaivola, Using Automata to Characterise Fixed Point Temporal Logics, PhD thesis, University of Edinburgh, Dept. of Computer Science, Report CST-135-97, April 1997.

A. Mader, Verification of Modal Properties Using Boolean Equation Systems, PhD thesis, Fakultät für Informatik, Technische Universität München, September 1997.

A. Arnold, An initial semantics for the mu-calculus on trees and Rabin's complementation lemma, Research Report, University of Bordeaux, 1997.

A. Arnold, The mu-calculus on trees and Rabin's complementation theorem, Research Report, University of Bordeaux, 1997.

D. E. Muller and P. E. Schupp, Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra, Theoretical Computer Science 141 (1995), 69-107.

Announcements

Final exam solutions are posted. That's all, folks! Thanks to everyone for their participation in the course. Have a great summer.

Homework 1    Solutions
Homework 2    Solutions
A few homework problems on topology from F98    Solutions
Homework 3    Solutions
Homework 4    Solutions
Notes on Safra's construction   
Final exam    Solutions

Last updated: 25 May 2001