Handling Non-linear Operations in the Value Analysis of COSTA
| Autor: | Diego Alonso, Puri Arenas, Samir Genaim |
|---|---|
| Rok vydání: | 2011 |
| Předmět: |
Class (computer programming)
Theoretical computer science General Computer Science Computer science Value (computer science) 020207 software engineering 02 engineering and technology Base (topology) bit arithmetic operations Theoretical Computer Science Polyhedron Resource (project management) Resource usage analysis value analysis 0202 electrical engineering electronic engineering information engineering Overhead (computing) 020201 artificial intelligence & image processing non-linear operations Computer Science(all) |
| Zdroj: | Electronic Notes in Theoretical Computer Science |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2011.11.002 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect