BRICS · Contents · Programme

Expressiveness and Complexity of Program Logics

A BRICS Mini-Course
April 23, 24 and 27, May 6, 1998

Lectures by
Igor Walukiewicz
Department of Informatics, Warsaw University, Poland

Course Contents

We will consider second order theories that have found applications in program verification and other areas of computer science. We will consider first and second order logics over words and trees. We will also discuss temporal logics and the mu-calculus over these structures. Finally we will consider all these logics over traces. We will be interested in the expressive power of these logics and the complexity of the satisfiability and the model checking problems.

Although we will approach the subject from the program verification perspective we hope that especially complexity issues may be of broader interest as the theories we will discuss proved to be a convenient tool for establishing the complexity of many problems in computer science.


Thursday April 23, 1998, 15:15-17:00 in Auditorium D3

Friday April 24, 1998, 13:15-15:00 in Auditorium D4

Monday April 27, 1998, 10:15-12:00 in Auditorium D1

Wednesday May 6, 1998, 13:15-14:00 in Colloquium B4