#
CS686 Spring 01

Logics of Programs

Course Information

## Instructor

## Time and Place

MW 1:15-2:30, Hollister 306.

## Office Hours

By appointment. Please contact Rosemary
Adessa, 5147 Upson, 255-9555.

## Workload & Grading

Workload will be minimal. Occasional readings as assigned. Optional homework exercises. Final paper,
project, or exam at the student's option.

## Topics

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

## Sources

*Dynamic Logic* by Harel, Kozen, and Tiuryn. 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.

##
Announcements

Final exam solutions are posted. That's all, folks! Thanks to everyone for their participation in the course. Have a great summer.

Homework 1
Solutions

Homework 2
Solutions

A few homework problems on topology from F98
Solutions

Homework 3
Solutions

Homework 4
Solutions

Notes on Safra's construction

Final exam
Solutions

##### Last updated: 25 May 2001