Automatic Generation of Local Repairs for Boolean Programs
- 1 November 2008
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Automatic techniques for software verification focus on obtaining witnesses of program failure. Such counterexamples often fail to localize the precise cause of an error and usually do not suggest a repair strategy. We present an efficient algorithm to automatically generate a repair for an incorrect sequential Boolean program where program correctness is specified using a pre-condition and a post-condition. Our approach draws on standard techniques from predicate calculus to obtain annotations for the program statements. These annotations are then used to generate a synthesis query for each program statement, which if successful, yields a repair. Furthermore, we show that if a repair exists for a given program under specified conditions, our technique is always able to find it.Keywords
This publication has 16 references indexed in Scilit:
- Fault Localization and Correction with QBFPublished by Springer Science and Business Media LLC ,2007
- Repair of Boolean Programs with an Application to CLecture Notes in Computer Science, 2006
- Revising UNITY Programs: Possibilities and LimitationsLecture Notes in Computer Science, 2006
- Error explanation with distance metricsInternational Journal on Software Tools for Technology Transfer, 2005
- Program Repair as a GameLecture Notes in Computer Science, 2005
- Finding and Fixing FaultsLecture Notes in Computer Science, 2005
- Fate and free will in error tracesInternational Journal on Software Tools for Technology Transfer, 2004
- Synthesis of fault-tolerant concurrent programsACM Transactions on Programming Languages and Systems, 2004
- Software Verification with BLASTLecture Notes in Computer Science, 2003
- Enhancing model checking in verification by AI techniquesArtificial Intelligence, 1999