The Library

A formal approach to fixing bugs

Tools

Kalvala, Sara and Warburton, Richard (2011) A formal approach to fixing bugs. In: Simao, A. and Morgan, C., (eds.) Formal methods, foundations and applications. Lecture Notes in Computer Science, Volume 7021 . Berlin: Springer-Verlag, pp. 172-187. ISBN 9783642250316

Preview

PDF
WRAP_Kalvala_postprint.pdf - Accepted Version - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (475Kb) | Preview

PDF
main.pdf - Published Version
Restricted to Repository staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (244Kb)

Official URL: http://dx.doi.org/10.1007/978-3-642-25032-3_12

Abstract

Bugs within programs typically arise within well-known motifs, such as complex language features or misunderstood programming interfaces. Some software development tools often detect some of these situations, and some integrated development environments suggest automated fixes for some of the simple cases. However, it is usually difficult to hand-craft and integrate more complex bug-fixing into these environments. We present a language for specifying program transformations which is paired with a novel methodology for identifying and fixing bug patterns within Java source code. We propose a combination of source code and bytecode analyses: this allows for using the control flow in the bytecode to help identify the bugs while generating corrected source code. The specification language uses a combination of syntactic rewrite rules and dataflow analysis generated from temporal logic based conditions. We demonstrate the approach with a prototype implementation.

Item Type:

Book Item

Subjects:

Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software

Divisions:

Faculty of Science > Computer Science

Library of Congress Subject Headings (LCSH):

Java (Computer program language), Debugging in computer science, Formal methods (Computer science)

Series Name:

Lecture Notes in Computer Science

Publisher:

Springer-Verlag

Place of Publication:

Berlin

ISBN:

9783642250316

ISSN:

0302-9743

Book Title:

Formal methods, foundations and applications

Editor:

Simao, A. and Morgan, C.

Official Date:

2011

Dates:

Date	Date Type
2011	Published

Volume:

Volume 7021

Page Range:

pp. 172-187

Identification Number:

10.1007/978-3-642-25032-3_12

Status:

Peer Reviewed

Publication Status:

Published

Access rights to Published version:

Restricted or Subscription Access

Description:

Proceedings of 14th Brazilian Symposium, SBMF 2011, Sao Paulo, September 26-30 2011

Funder:

Engineering and Physical Sciences Research Council (EPSRC)

Grant number:

EP/DO32466/1 (EPSRC)

Conference Paper Type:

Paper

Title of Event:

14th Brazilian Symposium, SBMF 2011

Type of Event:

Other

Location of Event:

São Paulo, Brazil

Date(s) of Event:

26-30 Sep 2011

References:

[1] Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Je.rey D. Ullman. Compilers:
Principles, Techniques, and Tools. Pearson Education, 2007.
[2] Eric Bruneton, Romain Lenglet, and Thierry Coupaye. ASM: a code manipulation
tool to implement adaptable systems. In Adaptable and Extensible
Component Systems, 2002.
[3] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of
finite-state concurrent systems using temporal logic specifications. ACM
Transactions on Programming Languages and Systems, 8:244–263, 1996.
[4] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization
skeletons using branching-time temporal logic. In Logic of
Programs, Workshop, pages 52–71, London, UK, 1982. Springer-Verlag.
[5] Eclipse Foundation. Eclipse website, 2009. http://www.eclipse.org.
[6] Michael D. Ernst. Type Annotations Specification (JSR 308). http://
types.cs.washington.edu/jsr308/, October 5, 2009.
[7] Michael D. Ernst, Je. H. Perkins, Philip J. Guo, Stephen McCamant, Carlos
Pacheco, Matthew S. Tschantz, and Chen Xiao. The Daikon system for
dynamic detection of likely invariants. Science of Computer Programming,
69(1–3):35–45, December 2007.
[8] David Hovemeyer and William Pugh. Finding bugs is easy. ACM SIGPLAN
Notices, 39(12):92–106, 2004.
[9] Sara Kalvala, Richard Warburton, and David Lacey. Program transformations
using temporal logic side conditions. ACM Transactions on Programming
Languages and Systems (TOPLAS), 31(4), 2009.
[10] Aditya Kanade, Amitabha Sanyal, and Uday Khedker. A PVS based framework
for validating compiler optimizations. In SEFM ’06: Proceedings of
the Fourth IEEE International Conference on Software Engineering and
Formal Methods, Washington, DC, USA, 2006. IEEE Computer Society.
[11] David Lacey. Program Transformation using Temporal Logic Specifications.
PhD thesis, Oxford University Computing Laboratory, 2003.
[12] S. Lerner, T. Millstein, and C. Chambers. Automatically proving the
correctness of compiler optimizations. In Proceedings of the ACM SIG-
PLAN 2003 conference on Programming language design and implementation.
ACM Press, 2003.
[13] Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers. Automated
soundness proofs for dataflow analyses and transformations via local rules.
In POPL ’05: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, pages 364–377, New York,
NY, USA, 2005. ACM Press.
[14] S. Muchnick. Advanced Compiler Design and Implementation. Morgan
Kaufmann, 1997.
[15] Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala.
Artima Press, second edition, 2010.
[16] Roopsha Samanta, Jyotirmoy V. Deshmukh, and E. Allen Emerson. Automatic
generation of local repairs for boolean programs. In FMCAD, 2008.
[17] D.A. Schmidt and B. Ste.en. Data-flow analysis as model checking of
abstract interpretations. In G. Levi, editor, 5th Static Analysis Symposium,
volume 1503 of Lecture Notes in Computer Science, September 1998.
[18] Jorg Spieler. UCDetector: the Unnecessary Code Detector website, 2007.
URL: http://www.ucdetector.org.
[19] B. Ste.en. Generating data flow analysis algorithms from modal specifications.
Science of Computer Programming, 21:115–139, 1993.
[20] Richard Warburton and Sara Kalvala. From specification to optimisation:
An architecture for optimisation of Java bytecode. In Oege de Moor and Michael I. Schwartzbach, editors, Compiler Construction, 18th International
Conference, volume 5501 of Lecture Notes in Computer Science. Springer, 2009.