COM S 686: Logics of Programs

Cross-Listing: Not cross-listed.

Topics in logics of programs 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.

Offered: Spring only

Prerequisites: COM S 481, 682, and (Math 481 or Math/COM S 486).

Grade options: Letter or S/U

Credit hours: 4

Recent offerings:

• http://www.cs.cornell.edu/courses/cs686/2007sp
• http://www.cs.cornell.edu/courses/cs686/2003sp
  • Dexter Kozen
• http://www.cs.cornell.edu/courses/cs686/2001sp
  • Dexter Kozen