Current Announcements
[Click here for archived announcements.]
| Date | Topic | Description |
|---|---|---|
| Thu 12/9 | HW4 & 5 | HW4 grades are posted. I hope to have finished grading HW5 by this evening. |
| Thu 12/9 | Final Projects | I must have my grades in by noon 12/21 at the absolute latest. I am leaving for Amsterdam next Thursday 12/16 at 6pm. If you are not finished by then, I will grade them over the weekend. Please submit your materials to CMS. If you have more than one file, please put them in a .zip archive. CMS is set not to accept submissions after 11:59pm EST 12/18. |
| Thu 12/9 | Final Exam | The final exam is ready for those who wish to take it. 72-hour takehome, open book and notes. Submit the completed exam to CMS. No collaboration please. Send me email for clarifications. |
Course Info
Overview
CS 6860 (formerly 686) 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, the Rabin tree theorem, the modal mu-calculus, games and alternating automata, applications to type inference, set constraints, Kleene algebra and Kleene algebra with tests.
Time & Place
10:10–11:25am TR, Upson 211
Staff
| POSITION | NAME | CONTACT | OFFICE HOURS |
|---|---|---|---|
| Instructor | Dexter Kozen |
Turn on JavaScript to view email address
255-9209 w 257-4579 h 592-2437 m |
5143 Upson WR 1:15–2:30pm or by appt |
| TA | In my dreams | ||
| Administrative Support | Randy Hess |
Turn on JavaScript to view email address
255-0985 w |
5147 Upson M–F 8:30am–4pm |
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.
6 homework assignments with 4–6 problems each, 50% of grade.
You may work with a partner.
Final paper, project, or 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.
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
Notes on Probabilistic PDL
HKT Chapters 11–17 + index
Approximate Syllabus
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