Course Info
Overview
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.
Prerequisites
CS 4810, CS 6110, and MATH 4810, or permission.
Time & Place
MW 9:40am - 10:55am
https://cornell.zoom.us/j/94751769913?pwd=TXBBWUMyaHlvbC9JeFo5cXptaG51Zz09 (Links to an external site.)
Staff
| POSITION | NAME | CONTACT | OFFICE HOURS |
|---|---|---|---|
| Instructor | Bob Constable | rc at cs dot cornell dot edu (607) 255.9204 |
By appointment only |
| TA | |||
| Administrative Support | Amy Elser | ahf42@cornell.edu |
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.
Handouts
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.