@inproceedings{gulavani2008a,
author = {Gulavani, Bhargav S. and Gulwani, Sumit},
title = {A Numerical Abstract Domain based on Expression Abstraction and Max Operator with Application in Timing Analysis},
booktitle = {CAV '08 Proceedings of the 20th international conference on Computer Aided Verification},
year = {2008},
month = {July},
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.},
publisher = {Springer-Verlag Berlin, Heidelberg},
url = {http://approjects.co.za/?big=en-us/research/publication/numerical-abstract-domain-based-expression-abstraction-max-operator-application-timing-analysis/},
pages = {370},
edition = {CAV '08 Proceedings of the 20th international conference on Computer Aided Verification},
}