 |
Dexter Kozen
kozen@cs.cornell.edu 5143 Upson 255-9209 office 257-4579 home |
MW 1:25-2:40, Upson 109
By appointment. Please contact Beth Howard, 5147 Upson, 255-4188
Occasional readings as assigned.
6 homework assignments with 4-6 problems each, 50% of grade.
Final paper,
project, or exam at the student's option, 50% of grade.
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
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.
HW 1, due Monday 2/3 Solutions
HW 2, due Monday 2/17 Solutions
HW 3, due Monday 3/3 Solutions
HW 4, due Wednesday 3/26
HW 5, due Friday 4/11
Safra's construction
If you downloaded HW4 before 5:48pm 3/6, please download it again. I have made a correction to Exercise 1.
I have discovered an erratum in the text that impacts Exercise 4 of HW4. Please see the latest version.