Record Details


Field	Value

Title	A numerical abstract domain based on expression abstraction and max operator with application in timing analysis

Names	GULAVANI, LS GULWANI, S
Date Issued	2008 (iso8601)
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.
Genre	Proceedings Paper
Topic	Predicate Abstraction
Identifier	COMPUTER AIDED VERIFICATION,5123,370-384

ICAR Research Data Repository for Knowledge Management