### Skapa referens, olika format (klipp och klistra)

**Harvard**

Albert, E., Bubel, R., Genaim, S., Hähnle, R. och Román-Díez, G. (2012) *Verified resource guarantees for heap manipulating programs*.

** BibTeX **

@conference{

Albert2012,

author={Albert, E. and Bubel, Richard and Genaim, S. and Hähnle, Reiner and Román-Díez, G.},

title={Verified resource guarantees for heap manipulating programs},

booktitle={Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012},

isbn={978-364228871-5},

pages={130-145},

abstract={Program properties that are automatically inferred by static analysis tools are generally not considered to be completely trustworthy, unless the tool implementation or the results are formally verified. Here we focus on the formal verification of resource guarantees inferred by automatic cost analysis. Resource guarantees ensure that programs run within the indicated amount of resources which may refer to memory consumption, to number of instructions executed, etc. In previous work we studied formal verification of inferred resource guarantees that depend only on integer data. In realistic programs, however, resource consumption is often bounded by the size of heap-allocated data structures. Bounding their size requires to perform a number of structural heap analyses. The contributions of this paper are (i) to identify what exactly needs to be verified to guarantee sound analysis of heap manipulating programs, (ii) to provide a suitable extension of the program logic used for verification to handle structural heap properties in the context of resource guarantees, and (iii) to improve the underlying theorem prover so that proof obligations can be automatically discharged.},

year={2012},

keywords={Cost analysis, Formal verifications, Memory consumption, Program logic, Program properties, Proof obligations, Resource consumption, Sound analysis, Theorem provers, Cost accounting, Data structures, Integer programming, Software engineering, Static analysis },

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 160193

A1 Albert, E.

A1 Bubel, Richard

A1 Genaim, S.

A1 Hähnle, Reiner

A1 Román-Díez, G.

T1 Verified resource guarantees for heap manipulating programs

YR 2012

T2 Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012

SN 978-364228871-5

SP 130

OP 145

AB Program properties that are automatically inferred by static analysis tools are generally not considered to be completely trustworthy, unless the tool implementation or the results are formally verified. Here we focus on the formal verification of resource guarantees inferred by automatic cost analysis. Resource guarantees ensure that programs run within the indicated amount of resources which may refer to memory consumption, to number of instructions executed, etc. In previous work we studied formal verification of inferred resource guarantees that depend only on integer data. In realistic programs, however, resource consumption is often bounded by the size of heap-allocated data structures. Bounding their size requires to perform a number of structural heap analyses. The contributions of this paper are (i) to identify what exactly needs to be verified to guarantee sound analysis of heap manipulating programs, (ii) to provide a suitable extension of the program logic used for verification to handle structural heap properties in the context of resource guarantees, and (iii) to improve the underlying theorem prover so that proof obligations can be automatically discharged.

LA eng

DO 10.1007/978-3-642-28872-2_10

LK http://dx.doi.org/10.1007/978-3-642-28872-2_10

OL 30