Record Details

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

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title A numerical abstract domain based on expression abstraction and max operator with application in timing analysis
 
Creator GULAVANI, LS
GULWANI, S
 
Subject predicate abstraction
linear ranking
programs
 
Description 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
 
Date 2011-10-24T00:05:43Z
2011-12-15T09:11:19Z
2011-10-24T00:05:43Z
2011-12-15T09:11:19Z
2008
 
Type Proceedings Paper
 
Identifier COMPUTER AIDED VERIFICATION,5123,370-384
978-3-540-70543-7
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15275
http://hdl.handle.net/100/1995
 
Source 20th International Conference on Computer Aided Verification,Princeton, NJ,JUL 07, 2008
 
Language English