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.
Abstract
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
@inproceedings{castano-lafm-2013,
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",
}