A formal verification framework for static analysis: As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY

Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of-the-art static analyzers typically combine a rang...

Full description

Saved in:
Bibliographic Details
Published in:Software and systems modeling 2016-10, Vol.15 (4), p.987-1012
Main Authors: Albert, Elvira, Bubel, Richard, Genaim, Samir, Hähnle, Reiner, Puebla, Germán, Román-Díez, Guillermo
Format: Article
Language:English
Subjects:
Analyzers
Compilers
Computer programs
Computer Science
Cost analysis
Information Systems Applications (incl.Internet)
Interpreters
IT in Business
Programming Languages
Programming Techniques
Software
Software Engineering
Software Engineering/Programming and Operating Systems
State of the art
Static code analysis
Systems analysis
Theme Section Paper
Translations
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of-the-art static analyzers typically combine a range of complex techniques, make use of external tools, and evolve quickly. To formally verify such systems is not a realistic option. In this work, we propose a different approach whereby, instead of the tools , we formally verify the results of the tools. The central idea of such a formal verification framework for static analysis is the method-wise translation of the information about a program gathered during its static analysis into specification contracts that contain enough information for them to be verified automatically. We instantiate this framework with costa , a state-of-the-art static analysis system for sequential Java programs, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Resource guarantees allow to be certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. Our results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.
ISSN:1619-1366
1619-1374
DOI:10.1007/s10270-015-0476-y