Skip to main content





Current Announcements

[Click here for archived announcements.]

Date Topic Description
Tue 3/11 Guest lectures Dexter will be out of town the week of 3/18. Fred Schneider will be the guest lecturer on Tuesday 3/19 and will speak on safety, liveness, and inline reference monitors. Joe Halpern will be the guest lecturer on Thursday 3/21 and will speak on modal logics of knowledge and belief. These will be fun lectures, so please attend!
Tue 3/11 Hoare logic notes The source for today's lecture on Cook's relative completeness theorem for Hoare logic can be found here.
Fri 3/8 HKT Ch. 11-17 Chapters 11-17 of HKT are available here.
Fri 3/8 Homework 3 HW3 has been released, due Monday 3/25. As before, you may work with a partner. If you do, please declare your partnership in CMS. Only one of you needs to submit the solutions.
Thu 2/14 HKT Ch. 4-10 Chapters 4-10 of HKT are available here.

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.
6 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

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.