Verified resource guarantees using COSTA and KeY

E Albert, R Bubel, S Genaim, R Hähnle… - Proceedings of the 20th …, 2011 - dl.acm.org
Proceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and …, 2011dl.acm.org
Resource guarantees allow being certain that programs will run within the indicated amount
of resources, which may refer to memory consumption, number of instructions executed, etc.
This information can be very useful, especially in real-time and safety-critical applications.
Nowadays, a number of automatic tools exist, often based on type systems or static analysis,
which produce such resource guarantees. In spite of being based on theoretically sound
techniques, the implemented tools may contain bugs which render the resource guarantees …
Resource guarantees allow being certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. This information can be very useful, especially in real-time and safety-critical applications. Nowadays, a number of automatic tools exist, often based on type systems or static analysis, which produce such resource guarantees. In spite of being based on theoretically sound techniques, the implemented tools may contain bugs which render the resource guarantees thus obtained not completely trustworthy. Performing full-blown verification of such tools is a daunting task, since they are large and complex. In this work we investigate an alternative approach whereby, instead of the tools, we formally verify the results of the tools. We have implemented this idea using COSTA, a state-of-the-art static analysis system, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Our preliminary results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.
ACM Digital Library
Showing the best result for this search. See all results