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

Content Provider	Springer Nature Link
Author	Albert, Elvira Bubel, Richard Genaim, Samir Hähnle, Reiner Puebla, Germán Román Díez, Guillermo
Copyright Year	2015
Abstract	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.
Starting Page	987
Ending Page	1012
Page Count	26
File Format	PDF
ISSN	16191366
Journal	Software and Systems Modeling
Volume Number	15
Issue Number	4
e-ISSN	16191374
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2015-07-15
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Cost analysis Closed-form upper bounds Resource analysis Resource guarantees Software Engineering/Programming and Operating Systems Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Information Systems Applications (incl. Internet) IT in Business
Content Type	Text
Resource Type	Article
Subject	Modeling and Simulation Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A Formal Verification Framework for Static Analysis ? As well as its instantiation to the resource analyzer costa and formal verification tool KeY

Formal verification of software source code through semi-automatic modeling

Formal verification of QVT transformations for code generation

The KeY tool : Integrating object oriented design and formal verification

Automated anonymity verification of the ThreeBallot and VAV voting systems

Theme issue on Integrated Formal Methods

Formal verification and validation of embedded systems: the UML-based MADES approach

Automated formal verification of visual modeling languages by model checking

Embedding domain-specific modelling languages in Maude specifications

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

Similar Documents

A Formal Verification Framework for Static Analysis ? As well as its instantiation to the resource analyzer costa and formal verification tool KeY

Formal verification of software source code through semi-automatic modeling

Formal verification of QVT transformations for code generation

The KeY tool : Integrating object oriented design and formal verification

Automated anonymity verification of the ThreeBallot and VAV voting systems

Theme issue on Integrated Formal Methods

Formal verification and validation of embedded systems: the UML-based MADES approach

Automated formal verification of visual modeling languages by model checking

Embedding domain-specific modelling languages in Maude specifications

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