Injecting Abstract Interpretations into Linear Cost Models

David Cachera
Arnaud Jobin

We present a semantics based framework for analysing the quantitative behaviour of programs with regard to resource usage. We start from an operational semantics equipped with costs. The dioid structure of the set of costs allows for defining the quantitative semantics as a linear operator. We then present an abstraction technique inspired from abstract interpretation in order to effectively compute global cost information from the program. Abstraction has to take two distinct notions of order into account: the order on costs and the order on states. We show that our abstraction technique provides a correct approximation of the concrete cost computations.

In Alessandra Di Pierro and Gethin Norman: Proceedings Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010), Paphos, Cyprus, 27-28th March 2010 , Electronic Proceedings in Theoretical Computer Science 28, pp. 64–81.
Published: 26th June 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.28.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org