FLoC '02 - CAV Saturday July 27th

CAV on Saturday

Detailed program
Saturday July 27th, 2002
See also the unified by-slot program

Sessions take place in auditorium 1 unless otherwise indicated.

Session 1: Tutorial I

Chair: Kim Guldstrand Larsen

09:00-

10:00

Wolfgang Thomas, Aachen U of Techn., Germany
Invited tutorial: Infinite games and verification
The purpose of this tutorial is to survey the essentials of the algorithmic theory of infinite games, its role in automatic program synthesis and verificaiton, and some challenges of current research.

10:00-

10:15

Coffee Break

10:15-

11:15

Wolfgang Thomas, Aachen U of Techn., Germany
continued: Infinite games and verification

Session 2: Tutorial IIa

Chair: Ed Brinksma

11:30-

12:30

Patrick Cousot, ENS Paris, France
Invited tutorial: On abstraction in software verification
We show that the precisiion of static abstract software checking algorithms can be enhanced by taking explicitely into account the abstractions that are involved in the design of the program model/abstract semantics. This is illustrated on reachability analysis and abstract testing.

Session 3: Tutorial IIb

Chair: Ed Brinksma

14:00-

15:00

Patrick Cousot, ENS Paris, France
continued: On abstraction in software verification

Session 4: Tutorial III

Chair: Jens Chr. Godskesen

15:15-

16:15

Thomas A. Henzinger, U California-Berkeley, USA
Invited tutorial: The symbolic approach to hybrid systems
A hybrid system is a dynamical system whose state has both a discrete component, which is updated in a sequence of steps, and a continuous component, which evolves over time. Hybrid systems are a useful modeling tool in a variety of situations, including the embedded (digital) control of physical (analog) plants, robotics, circuits, biology, and finance.
We survey a computational approach to the verification and control of hybrid systems which is based on the symbolic discretization of continuous state changes. On the theoretical side, we classify infinite, hybrid state spaces as to which finite, discrete abstractions they admit. This classification enables us to apply concepts and results from concurrency theory, model checking, and game theory to hybrid systems. On the practical side, we discuss several options for implementing the symbolic approach to hybrid systems, and point to existing tool support.

16:15-

16:30

Coffee Break

16:30-

17:30

Thomas A. Henzinger, U California-Berkeley, USA
continued: The symbolic approach to hybrid systems

17:30-19:00 Welcome reception

Joint with CADE
Room: Lobby