NDLI: Program Repair as Sound Optimization of Broken Programs

Content Provider	IEEE Xplore Digital Library
Author	Fischer, B. Saabas, A. Uustalu, T.
Copyright Year	2009
Abstract	We present a new, semantics-based approach to mechanical program repair where the intended meaning of broken programs (i.e., programs that may abort under a given, error-admitting language semantics) can be defined by a special, error-compensating semantics. Program repair can then become a compile-time, mechanical program transformation based on a program analysis. It turns a given program into one whose evaluations under the error-admitting semantics agree with those of the given program under the error-compensating semantics. We present the analysis and transformation as a type system with a transformation component, following the type-systematic approach to program optimization from our earlier work. The type-systematic method allows for simple soundness proofs of the repairs, based on a relational interpretation of the type system, as well as mechanical transformability of program correctness proofs between the Hoare logics for the error-compensating and error-admitting semantics. We first demonstrate our approach on the repair of file-handling programs with missing or superfluous open and close statements. Our framework shows that this repair is strikingly similar to partial redundancy elimination optimization commonly used by compilers. In a second example, we demonstrate the repair of programs operating a queue that can over- and underflow, including mechanical transformation of program correctness proofs.
Starting Page	165
Ending Page	173
File Size	251986
Page Count	9
File Format	PDF
ISBN	9780769537573
DOI	10.1109/TASE.2009.61
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2009-07-29
Publisher Place	China
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Optimizing compilers Redundancy similarity relations program repair Programming profession Cybernetics type systems Computer science Runtime mechanical transformation of program correctness proofs program optimization soundness Computer errors Error correction Logic program logics Software engineering
Content Type	Text
Resource Type	Article

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

Syntactic Error Correction in Programming Languages

Program decision logic optimization using predication and control speculation

The Logic of Computer Programming

Transformation of path information for WCET analysis during compilation

Runtime Validation of Transactional Memory Systems

Verifying asymptotic correctness

A critique of the foundations of Hoare style programming logics

Program repair as sound optimization of broken programs.

Constraint-based correctness proofs for logic program transformations

Program Repair as Sound Optimization of Broken Programs

Similar Documents

Syntactic Error Correction in Programming Languages

Program decision logic optimization using predication and control speculation

The Logic of Computer Programming

Transformation of path information for WCET analysis during compilation

Runtime Validation of Transactional Memory Systems

Verifying asymptotic correctness

A critique of the foundations of Hoare style programming logics

Program repair as sound optimization of broken programs.

Constraint-based correctness proofs for logic program transformations

Program Repair as Sound Optimization of Broken Programs