On Verifying Resource Contracts using Code Contracts - LAFM 2013
by Rodrigo Casta˝o, Juan Pablo Galeotti, Diego Garbervetsky, Jonathan Tapicer, Edgardo Toppi

Nazareno Aguirre, Leila Ribeiro (Ed.), Pages 1-15, Electronic Proceedings in Theoretical Computer Science, Volume 139, Open Publishing Association, January 2014.

Digital Library via DOI: 10.4204/EPTCS.139.1 - Local copy: Download as PDF file.


In this paper we present an approach to check resource consumption contracts using an off-the-shelf static analyzer. We propose a set of annotations to support resource usage specifications, in particular, dynamic memory consumption constraints. Since dynamic memory may be recycled by a memory manager, the consumption of this resource is not monotone. The specification language can express both memory consumption and lifetime properties in a modular fashion. We develop a proof-of-concept implementation by extending Code Contracts' specification language. To verify the correctness of these annotations we rely on the Code Contracts static verifier and a points-to analysis. We also briefly discuss possible extensions of our approach to deal with non-linear expressions.

BibTeX Entry

    title = "On Verifying Resource Contracts using Code Contracts",
    author = "Rodrigo Casta˝o and Juan Pablo Galeotti and Diego Garbervetsky and Jonathan Tapicer and Edgardo Toppi",
    year = "2014",
    month = jan,
    editors = "Nazareno Aguirre and Leila Ribeiro",
    pages = "1--15",
    publisher = "Open Publishing Association",
    series = "Electronic Proceedings in Theoretical Computer Science",
    volume = "139",
    doi = "10.4204/EPTCS.139.1",

Show all publications of the Software Engineering Chair.