On verifying resource contracts using code contracts

In this paper we present an approach to check resource consumption contracts using an off-theshelf 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 manage...

Descripción completa

Detalles Bibliográficos
Autores principales: Garbervetsky, Diego, Tapicer, Jonathan, Galeotti, Juan Pablo
Publicado: 2014
Materias:
Computational linguistics
Formal methods
Specification languages
Specifications
Dynamic memory
Memory consumption
Memory manager
Points-to analysis
Proof of concept
Resource consumption
Resource usage
Static analyzers
Codes (symbols)
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_20752180_v139_n_p1_Castano
http://hdl.handle.net/20.500.12110/paper_20752180_v139_n_p1_Castano
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_20752180_v139_n_p1_Castano
record_format dspace
spelling paper:paper_20752180_v139_n_p1_Castano2023-06-08T16:34:13Z On verifying resource contracts using code contracts Garbervetsky, Diego Tapicer, Jonathan Galeotti, Juan Pablo Computational linguistics Formal methods Specification languages Specifications Dynamic memory Memory consumption Memory manager Points-to analysis Proof of concept Resource consumption Resource usage Static analyzers Codes (symbols) In this paper we present an approach to check resource consumption contracts using an off-theshelf 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. © 2014 Pablo F. Castro & Thomas S. E. Maibaum. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Tapicer, J. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Galeotti, J.P. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_20752180_v139_n_p1_Castano http://hdl.handle.net/20.500.12110/paper_20752180_v139_n_p1_Castano
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Computational linguistics
Formal methods
Specification languages
Specifications
Dynamic memory
Memory consumption
Memory manager
Points-to analysis
Proof of concept
Resource consumption
Resource usage
Static analyzers
Codes (symbols)
spellingShingle Computational linguistics
Formal methods
Specification languages
Specifications
Dynamic memory
Memory consumption
Memory manager
Points-to analysis
Proof of concept
Resource consumption
Resource usage
Static analyzers
Codes (symbols)
Garbervetsky, Diego
Tapicer, Jonathan
Galeotti, Juan Pablo
On verifying resource contracts using code contracts
topic_facet Computational linguistics
Formal methods
Specification languages
Specifications
Dynamic memory
Memory consumption
Memory manager
Points-to analysis
Proof of concept
Resource consumption
Resource usage
Static analyzers
Codes (symbols)
description In this paper we present an approach to check resource consumption contracts using an off-theshelf 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. © 2014 Pablo F. Castro & Thomas S. E. Maibaum.
author Garbervetsky, Diego
Tapicer, Jonathan
Galeotti, Juan Pablo
author_facet Garbervetsky, Diego
Tapicer, Jonathan
Galeotti, Juan Pablo
author_sort Garbervetsky, Diego
title On verifying resource contracts using code contracts
title_short On verifying resource contracts using code contracts
title_full On verifying resource contracts using code contracts
title_fullStr On verifying resource contracts using code contracts
title_full_unstemmed On verifying resource contracts using code contracts
title_sort on verifying resource contracts using code contracts
publishDate 2014
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_20752180_v139_n_p1_Castano
http://hdl.handle.net/20.500.12110/paper_20752180_v139_n_p1_Castano
work_keys_str_mv AT garbervetskydiego onverifyingresourcecontractsusingcodecontracts
AT tapicerjonathan onverifyingresourcecontractsusingcodecontracts
AT galeottijuanpablo onverifyingresourcecontractsusingcodecontracts
_version_ 1768543679392251904

Ejemplares similares