Skip to main content

Current Announcements

[Click here for archived announcements.]

Date Topic Description
Fri 5/24 That's all folks! Final grades are in. Thanks to all for an enjoyable semester. Have a great summer!

Course Info


CS 6860 is a course on program logics and program verification. Possible topics include: Floyd/Hoare logic, modal logic, dynamic logic, temporal logic, process logic, automata on infinite objects and their relation to program logics, model checking, applications to type inference, set constraints, Kleene algebra and Kleene algebra with tests, the modal mu-calculus, constructive and intuitionistic logics, the propositions-as-types principle, inductive and co-inductive types, games and alternating automata.


CS 4810, CS 6110, and MATH 4810, or permission.

Time & Place

10:10–11:25am TR, Phillips 203


Instructor Dexter Kozen Turn on JavaScript to view email address
607-255-9209 w
607-257-4579 h
607-592-2437 m
436 Gates
TR 11:30am–12:15pm
or by appt
TA In my dreams
Administrative Support Corey Torres Turn on JavaScript to view email address
607-255-9197 w
401 Gates
M–F 8am–4:30pm


The course website is Announcements will be posted on the home page. Check frequently for new announcements.

Workload & Grading

Occasional readings as assigned.
Occasional homework assignments with 4–6 problems each, 50% of grade. You may work with a partner.
Final paper, project, or takehome exam at the student's option, 50% of grade. This is to be done individually.


Homework should be in .pdf format and should be submitted to CMS. If you work with a partner, please form a group in CMS. Only one person needs to submit the homework. Click here to login.

Sources (recommended, not required)

Dynamic Logic by Harel, Kozen, and Tiuryn (HKT).  MIT Press, 2000. [Ch. 1-3] [Ch. 4-10] [Ch. 11-17]
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.
E. A. Emerson and C. S. Jutla, Tree Automata, Mu-Calculus, and Determinacy.
Arnold Beckmann and Faron Moller, On the Complexity of Parity Games.
Henryk Björklund, Sven Sandberg, and Sergei Vorobyov, Memoryless Determinacy of Parity and Mean Payoff Games: A Simple Proof.


HKT Chapters 1–3
Survey paper on Hoare Logic
HKT Chapters 4–10
HKT Chapters 11–17 + index
Thomas: Languages, Automata, Logic (material on S1S and ω-automata)
notes on Safra's construction
Statman: PSPSACE-completeness of intuitionistic propositional logic
Notes on Probabilistic PDL

Academic Integrity

It goes without saying that the utmost degree of academic integrity is expected of everyone. Please familiarize yourself with The Essential Guide to Academic Integrity at Cornell. Acknowledge all sources, including Internet sources and other students with whom you discussed ideas. It is ok to discuss ideas with others as long as you acknowledge them.

Special Needs

Special needs will be accommodated. Please let me know as soon as possible.