Campus Event Calendar
Event Entry
What and Who
Abstract Interpretation with Applications to Timing Analysis
Reinhard Wilhelm
Saarland University
Virtual Seminar
AG 1, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 9 January 2009
13:30
60 Minutes
E1 4
019
Saarbrücken
Abstract
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.
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.
Contact
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 01/07/2009 08:20 -- Created document.