Skip to main content


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

MW 9:40am - 10:55am (Links to an external site.)


Instructor Bob Constable rc at cs dot cornell dot edu
(607) 255.9204
By appointment only
Administrative Support Amy Elser  

Sources (recommended, not required)

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.


Intuitionistic Math and Logic

Logic History


Lecture 1

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.