Observatorio de I+D+i UPM

Memorias de investigación
Communications at congresses:
Handling Non-linear Operations in the Value Analysis of COSTA
Year:2011
Research Areas
  • Programming language
Information
Abstract
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.
International
Si
Congress
Sixth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode'11)
960
Place
Saarbrucken, Germany
Reviewers
Si
ISBN/ISSN
1571-0661
Start Date
27/03/2011
End Date
27/03/2011
From page
3
To page
17
Proceedings of the Bytecode 2011 workshop, the Sixth Workshop on Bytecode Semantics, Verification, Analysis and Transformation
Participants
  • Autor: Diego Alonso (Universidad Complutense de Madrid)
  • Autor: Purificación Arenas Sánchez (UPM)
  • Autor: Samir Genaim . (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: Computación lógica, Lenguajes, Implementación y Paralelismo (CLIP)
  • Departamento: Inteligencia Artificial
S2i 2020 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)