|
Descripción
|
|
|---|---|
| Inferring precise relations between (the values of) program variables at different program points is essential for termination and resource usage analysis. In both cases, this information is used to synthesize ranking functions that imply the program's termination and bound the number of iterations of its loops. For efficiency, it is common to base value analysis on non-disjunctive abstract domains such as Polyhedra, Octagon, etc. While these domains are efficient and able to infer complex relations for a wide class of programs, they are often not sufficient for modeling the effect of non-linear and bit arithmetic operations. Modeling such operations precisely can be done by using more sophisticated abstract domains, at the price of performance overhead. In this paper we report on the value analysis of COSTA that is based on the idea of encoding the disjunctive nature of non-linear operations into the (abstract) program itself, instead of using more sophisticated abstract domains. Our experiments demonstrate that COSTA is able to prove termination and infer bounds on resource consumption for programs that could not be handled before. | |
|
Internacional
|
Si |
|
Nombre congreso
|
Sixth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode'11) |
|
Tipo de participación
|
960 |
|
Lugar del congreso
|
Saarbrucken, Germany |
|
Revisores
|
Si |
|
ISBN o ISSN
|
1571-0661 |
|
DOI
|
|
|
Fecha inicio congreso
|
27/03/2011 |
|
Fecha fin congreso
|
27/03/2011 |
|
Desde la página
|
3 |
|
Hasta la página
|
17 |
|
Título de las actas
|
Proceedings of the Bytecode 2011 workshop, the Sixth Workshop on Bytecode Semantics, Verification, Analysis and Transformation |