Tuesday 24 August 2004
Organizer:
Patrick Cousot (ƒcole Normale SupŽrieure, Paris,
France)
Abstract Interpretation is a theory of
approximation of mathematical structures, in particular those involved in the
semantic models of computer systems. Abstract interpretation can be applied to
the systematic construction of methods and effective algorithms to approximate
undecidable or very complex problems in computer science such that the
semantics, the proof, the static analysis, the verification, the safety and the
security of software or hardware computer systems. In particular, the static
analysis by abstract interpretation, which automatically infers dynamic
properties of computer systems, has been very successful these last years to
automatically verify complex properties of real-time, safety critical, embedded
systems.
The
topical day is a vertical presentation of abstract interpretation from theory
to practice, including an informal introduction to abstract interpretation, the
presentation of static analysis tools and the assessment of
their use in an industrial context at Airbus France.
10h30
Ð 12h
Session 1: Foundations
Chair : Famantanantsoa Randimbivololona (Airbus France,
Toulouse)
Basic concepts of abstract
interpretation Ð Patrick Cousot (ƒcole
Normale SupŽrieure, Paris,
France)
13h30
Ð 15h
Session 2: Tools
Chair: Radhia Cousot (ƒcole Polytechnique, Palaiseau,
France)
TVLA : A system for generating
abstract interpreters Ð Mooly Sagiv (Te-Aviv
U., Israel)
AiT: worst case execution time Ð Christian Ferdinand (AbsInt GmbH, Saarbruecken, Germany)
15h30
Ð 17h
Chair: Radhia Cousot (ƒcole Polytechnique, Palaiseau,
France)
AstrŽe: verification of absence of run-time errors Ð Laurent Mauborgne (ƒcole Normale SupŽrieure,
Paris, France)
Experience with the industrial use of abstract
interpretation-based static analysis tools Ð Jean Souyris (Airbus
France, Toulouse)