(BA) Trace refinement with reduced interpolant automata for binary programs

Betreuer: Frank Ortmeier,Michael Lipaczewski
Student: Severin Orth
Zeitraum: 1.7. - 23.09.2015

Static timing analysis relies on an abstraction of the model.
Because the abstraction covers a larger space than the original, proofs may be spurious.
For example, when calculating worst case execution times in an abstraction one may discover that the path is actually infeasible in the real program.
In this thesis we focus on refinement of trace abstractions with canonical interpolant automata using satisfiability modulo theory.
Using interpolants helps to refine abstractions with recurring locations in a small number of iterations without requiring any manual annotations.
We show as well that with a projection on conditional instructions reduced abstractions are achieved that can be checked more efficiently.
To validate the approach an implementation in Python using the real-time model-checker UPPAAL and the SMT solver SMTInterpol
shows an application in calculating worst case execution time of binary programs for the ARM920T micro processor.

Severin Orth: Trace refinement with reduced interpolant automata for binary programs. Otto-von-Guericke-Universität Magdeburg, 2015.
(BA) Trace refinement with reduced interpolant automata for binary programs