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
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
10:10–11:25am TR, Phillips 203
Staff
POSITION | NAME | CONTACT | OFFICE HOURS |
---|---|---|---|
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 |
Website
The course website is http://www.cs.cornell.edu/Courses/cs6860/. 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.
CMS
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.
Handouts
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.