NDLI: Verified resource guarantees using COSTA and KeY

Please wait, while we are loading the content...

A walk in the semantic park

Partial evaluation of the reversible language janus

A generative geometric kernel

Verified resource guarantees using COSTA and KeY

DiaSuite: a paradigm-oriented software development approach

Probabilistic accuracy bounds for perforated programs: a new foundation for program analysis and transformation

Calculating with lenses: optimising bidirectional transformations

A program transformation for returning states in functional-logic programs

Strictification of circular programs

Ordering multiple continuations on the stack

Taming code explosion in supercompilation

An embedded language for programming protocol stacks in embedded systems

Adaptation-based programming in java

Calculating tree navigation with symmetric relational zipper

Type classes in functional logic programming

A semantics for lazy assertions

Allocation removal by partial evaluation in a tracing JIT

iTasks for a change: type-safe run-time change in dynamically evolving workflows

Verified resource guarantees using COSTA and KeY

Content Provider	ACM Digital Library
Author	Genaim, Samir Román-Díez, Guillermo Albert, Elvira Hähnle, Reiner Puebla, Germán Bubel, Richard
Abstract	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.
Starting Page	73
Ending Page	76
Page Count	4
File Format	PDF
ISBN	9781450304856
DOI	10.1145/1929501.1929513
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2011-01-24
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Java Resource guarantees Static analysis
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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