CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verified Resource Guarantees using COSTA and KeY

Elvira Albert ; Richard Bubel (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Samir Genaim ; Reiner Hähnle (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; German Puebla ; Guillermo Roman-Diez
Proc. ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation (PEPM'11), ACM Press p. 73-76. (2011)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Java, Resource guarantees, Static analysis



Denna post skapades 2010-11-19. Senast ändrad 2011-03-23.
CPL Pubid: 129289

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)