research-article

Free access

Automatic generation of local repairs for Boolean programs

Authors:

Roopsha Samanta,

Jyotirmoy V. Deshmukh,

E. Allen EmersonAuthors Info & Claims

FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design

Article No.: 27, Pages 1 - 10

Published: 17 November 2008 Publication History

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.

References

[1]

P. C. Attie, A. Arora, and E. A. Emerson, "Synthesis of Fault-tolerant Concurrent Programs," ACM Trans. Program. Lang. Syst., vol. 26, no. 1, pp. 125--185, 2004.

Digital Library

[2]

T. Ball and S. K. Rajamani, "Boolean Programs: A Model and Process for Software Analysis."

[3]

T. Ball and S. K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces," in Proceedings of the 8th International Workshop on Model Checking of Software (SPIN). Springer-Verlag, 2001, pp. 103--122.

Digital Library

[4]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, "Software Verification with BLAST," in Proceedings of the 10th International Workshop on Model Checking of Software (SPIN), 2003, pp. 235--239.

Digital Library

[5]

K. M. Chandy and J. Misra, Parallel Program Design: A Foundation. Addison-Wesley, 1988.

Digital Library

[6]

A. Griesmayer, R. Bloem, and B. Cook, "Repair of Boolean Programs with an Application to C," in 18th Conference on Computer Aided Verification (CAV), T. Ball and R. B. Jones, Eds., 2006, pp. 358--371.

Digital Library

[7]

B. Jobstmann, A. Griesmayer, and R. Bloem, "Program Repair as a Game," in 17th Conference on Computer Aided Verification (CAV), K. Etessami and S. K. Rajamani, Eds. Springer-Verlag, 2005, pp. 226--238.

Digital Library

[8]

S. Staber, B. Jobstmann, and R. Bloem, "Finding and Fixing Faults," in 13th Conference on Correct Hardware Design and Verification Methods (CHARME), D. Borrione and W. Paul, Eds. Springer-Verlag, 2005, pp. 35--49.

Digital Library

[9]

L. A. Dennis, "Program Slicing and Middle-Out Reasoning for Error Location and Repair," in Disproving: Non-Theorems, Non-Validity and Non-Provability, 2006.

[10]

L. A. Dennis, R. Monroy, and P. Nogueira, "Proof-directed Debugging and Repair," in Seventh Symposium on Trends in Functional Programming, H. Nilsson and M. van Eekelen, Eds., 2006, pp. 131--140.

[11]

F. Buccafurri, T. Eiter, G. Gottlob, and N. Leone, "Enhancing Model Checking in Verification by AI Techniques," Artif. Intell., vol. 112, no. 1--2, pp. 57--104, 1999.

Digital Library

[12]

Y. Zhang and Y. Ding, "CTL Model Update for System Modifications," J. of Artif. Intell. Res., vol. 31, pp. 113--155, 2008.

Digital Library

[13]

P. C. Attie and J. Saklawi, "Model and Program Repair via SAT Solving," Tech. Rep., 2007.

[14]

A. Ebnenasir, S. S. Kulkarni, and B. Bonakdarpour, "Revising UNITY Programs: Possibilities and Limitations," in International Conference on Principles of Distributed Systems (OPODIS), 2005, pp. 275--290.

Digital Library

[15]

A. Solar-Lezama, R. Rabbah, R. Bodik, and K. Ebcioglu, "Programming by Sketching for Bit-streaming Programs," in ACM SIGPLAN conference on Programming language design and implementation (PLDI). ACM, 2005, pp. 281--294.

Digital Library

[16]

A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat, "Combinatorial Sketching for Finite Programs," in 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM, 2006, pp. 404--415.

Digital Library

[17]

S. Staber and R. Bloem, "Fault Localization and Correction with QBF," in Tenth International Conference on Theory and Applications of Satisfiability Testing (SAT), 2007.

Digital Library

[18]

A. Groce, S. Chaki, D. Kroening, and O. Strichman, "Error Explanation with Distance Metrics," Int. J. Softw. Tools Technol. Transf., vol. 8, no. 3, pp. 229--247, 2006.

Digital Library

[19]

T. Ball, M. Naik, and S. K. Rajamani, "From Symptom to Cause: Localizing Errors in Counterexample Traces," in Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL). ACM, 2003, pp. 97--105.

Digital Library

[20]

H. Jin, K. Ravi, and F. Somenzi, "Fate and Free Will in Error Traces," Int. J. Softw. Tools Technol. Transf., vol. 6, no. 2, pp. 102--116, 2004.

Digital Library

[21]

E. W. Dijkstra, A Discipline of Programming. Prentice Hall, 1976.

Digital Library

[22]

M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge Univeristy Press, 2004.

Digital Library

[23]

E. W. Dijkstra and C. S. Scholten, Predicate Calculus and Program Semantics. Springer-Verlag New York, Inc., 1990.

Digital Library

[24]

J. Whaley, "JavaBDD: An Efficient BDD Library for Java," http://javabdd.sourceforge.net/.

Cited By

Gember-Jacobson AAkella AMahajan RLiu H(2017)Automatically Repairing Network Control Planes Using an Abstract RepresentationProceedings of the 26th Symposium on Operating Systems Principles10.1145/3132747.3132753(359-373)Online publication date: 14-Oct-2017
https://dl.acm.org/doi/10.1145/3132747.3132753
Liang CBu LLi ZZhang JHan SKarlsson BZhang DZhao F(2016)Systematically Debugging IoT Control System Correctness for Building AutomationProceedings of the 3rd ACM International Conference on Systems for Energy-Efficient Built Environments10.1145/2993422.2993426(133-142)Online publication date: 16-Nov-2016
https://dl.acm.org/doi/10.1145/2993422.2993426
Roohitavaf MKulkarni S(2016)Stabilization and fault-tolerance in presence of unchangeable environment actionsProceedings of the 17th International Conference on Distributed Computing and Networking10.1145/2833312.2833324(1-10)Online publication date: 4-Jan-2016
https://dl.acm.org/doi/10.1145/2833312.2833324
Show More Cited By

Recommendations

Automatic predicate abstraction of C programs

Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of ...
Automatic predicate abstraction of C programs
PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation

Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of ...
Verification of Boolean programs with unbounded thread creation

Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design

November 2008

236 pages

ISBN:9781424427352

Editors:
Alessandro Cimatti
FBK-irst
,
Robert B. Jones
Intel Corporation

Sponsors

CEDA: Council on Electronic Design Automation

Publisher

IEEE Press

Publication History

Published: 17 November 2008

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
65
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)4

Reflects downloads up to 12 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gember-Jacobson AAkella AMahajan RLiu H(2017)Automatically Repairing Network Control Planes Using an Abstract RepresentationProceedings of the 26th Symposium on Operating Systems Principles10.1145/3132747.3132753(359-373)Online publication date: 14-Oct-2017
https://dl.acm.org/doi/10.1145/3132747.3132753
Liang CBu LLi ZZhang JHan SKarlsson BZhang DZhao F(2016)Systematically Debugging IoT Control System Correctness for Building AutomationProceedings of the 3rd ACM International Conference on Systems for Energy-Efficient Built Environments10.1145/2993422.2993426(133-142)Online publication date: 16-Nov-2016
https://dl.acm.org/doi/10.1145/2993422.2993426
Roohitavaf MKulkarni S(2016)Stabilization and fault-tolerance in presence of unchangeable environment actionsProceedings of the 17th International Conference on Distributed Computing and Networking10.1145/2833312.2833324(1-10)Online publication date: 4-Jan-2016
https://dl.acm.org/doi/10.1145/2833312.2833324
Černý PHenzinger TRadhakrishna ARyzhyk LTarrach T(2014)Regression-Free Synthesis for ConcurrencyProceedings of the 16th International Conference on Computer Aided Verification - Volume 855910.1007/978-3-319-08867-9_38(568-584)Online publication date: 18-Jul-2014
https://dl.acm.org/doi/10.1007/978-3-319-08867-9_38
Bonakdarpour BHajisheykhi RKulkarni S(2014)Knowledge-Based Automated Repair of Authentication ProtocolsProceedings of the 19th International Symposium on FM 2014: Formal Methods - Volume 844210.1007/978-3-319-06410-9_10(132-147)Online publication date: 12-May-2014
https://dl.acm.org/doi/10.1007/978-3-319-06410-9_10
Essen CJobstmann B(2013)Program Repair without RegretProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958066(896-911)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958066
Lin YBonakdarpour BKulkarni S(2013)Automated Addition of Fault-Tolerance under Synchronous Semantics15th International Symposium on Stabilization, Safety, and Security of Distributed Systems - Volume 825510.5555/2718693.2718712(266-280)Online publication date: 13-Nov-2013
https://dl.acm.org/doi/10.5555/2718693.2718712
Bodik RJobstmann B(2013)Algorithmic program synthesisInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0287-915:5-6(397-411)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1007/s10009-013-0287-9
Logozzo FBall T(2012)Modular and verified automatic program repairACM SIGPLAN Notices10.1145/2398857.238462647:10(133-146)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384626
Logozzo FBall TLeavens GDwyer M(2012)Modular and verified automatic program repairProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384626(133-146)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384626
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents