A Numerical Abstract Domain based on Expression Abstraction and Max Operator with Application in Timing Analysis
Abstract
This paper describes a precise numerical abstract domain for use in
timing analysis. The numerical abstract domain is parameterized by a
linear abstract domain and is constructed by means of two domain
lifting operations. One domain lifting operation is based on the principle of
expression abstraction (which involves defining a set of
expressions and specifying their semantics using a collection of
directed inference rules) and has a more general applicability. It
lifts any given abstract domain
to include reasoning about a given set of expressions whose semantics
is abstracted using a set of axioms.
The other domain lifting operation incorporates disjunctive reasoning into a
given linear relational abstract domain via
introduction of max expressions. We present experimental results
demonstrating the potential of the new numerical abstract domain to
discover a wide variety of timing bounds (including polynomial,
disjunctive, logarithmic, exponential, etc.) for small C programs.