On Verifying Resource Contracts using Code Contracts

Rodrigo Castaño
(Departamento de Computación. FCEyN. UBA)
Juan Pablo Galeotti
(Saarland University)
Diego Garbervetsky
(Departamento de Computación. FCEyN. UBA)
Jonathan Tapicer
(Departamento de Computación. FCEyN. UBA)
Edgardo Zoppi
(Departamento de Computación. FCEyN. UBA)

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.

In Nazareno Aguirre and Leila Ribeiro: Proceedings First Latin American Workshop on Formal Methods (LAFM 2013), Buenos Aires, Argentina, August 26th 2013, Electronic Proceedings in Theoretical Computer Science 139, pp. 1–15.
Published: 2nd January 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.139.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org