Search: onr:"swepub:oai:research.chalmers.se:82e1fb8c-bff1-4b49-a811-ddda8e4ef7f5" >
Verified resource g...
Verified resource guarantees for heap manipulating programs
-
- Albert, Elvira (author)
- Universidad Complutense de Madrid,Complutense University
-
- Bubel, Richard, 1976 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Genaim, Samir (author)
- Universidad Complutense de Madrid,Complutense University
-
show more...
-
- Hähnle, Reiner, 1962 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Roman-Diez, Guillermo (author)
- Universidad Politecnica de Madrid,Technical University of Madrid
-
show less...
-
(creator_code:org_t)
- ISBN 9783642288715
- Berlin, Heidelberg : Springer Berlin Heidelberg, 2012
- 2012
- English.
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642288715 ; 7212, s. 130-145
- Related links:
-
http://dx.doi.org/10...
-
show more...
-
https://link.springe...
-
https://doi.org/10.1...
-
https://research.cha...
-
show less...
Abstract
Subject headings
Close
- 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.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Keyword
- Proof obligations
- Static analysis
- Integer programming
- Program logic
- Formal verifications
- Program properties
- Cost accounting
- Resource consumption
- Theorem provers
- Sound analysis
- Cost analysis
- Software engineering
- Memory consumption
- Data structures
Publication and Content Type
- kon (subject category)
- ref (subject category)
Find in a library
To the university's database