Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Abstract Interpretation with Applications to Timing Analysis
Speaker:Reinhard Wilhelm
coming from:Saarland University
Speakers Bio:
Event Type:Virtual Seminar
Visibility:D1, RG1
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Friday, 9 January 2009
Duration:60 Minutes
Building:E1 4
Abstract interpretation is one of the main verification technologies
besides model checking  and deductive verification.
Model checking and abstract interpretation both compute properties
of programs or other systems by fixpoint iteration.

We explain abstract interpretation using examples from a particular
application domain, the determination of bounds on the execution
times of programs.These bounds are used to show reliably that
hard real-time systems satisfy their timing constraints.

The application domain is rich enough to offer a wealth of static analyses.
Some are obtained as Galois connections from the collecting semantics,
other that cannot be obtained by Galois connections,
some that satisfy the ascending chain condition and others that require
widening because their domains possess infinite ascending chains.
Run-time guarantees play an important role in the area of embedded
systems and especially hard real-time systems.  These bounds must
be safe, i.e., they may never underestimate the real execution time.
Furthermore, they should be tight, i.e., the overestimation should be as
small as possible.

In modern microprocessor architectures, caches, pipelines, and all kinds
of speculation are key features for improving (average-case) performance.
Unfortunately, they make the analysis of the timing behaviour of instructions
very difficult, since the execution time of an instruction depends on the
execution history.
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Jennifer Müller, 01/07/2009 08:20 AM -- Created document.