Abstract
A static program checker that performs modular checking can check one program module for errors without needing to analyze the entire program. Modular checking requires that each module be accom- panied by annotations that specify the module. To help reduce the cost of writing specifications, this paper presents Houdini, an annotation as- sistant for the modular checker ESC/Java. To infer suitable ESC/Java annotations for a given program, Houdini generates a large number of candidate annotations and uses ESC/Java to verify or refute each of these annotations. The paper describes the design, implementation, and preliminary evaluation of Houdini.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
William R. Bush, Jonathan D. Pincus, and David J. Sielaff. A static analyzer for finding dynamic programming errors. Software Practice & Experience, 30:775–802, 2000.
Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, January 1977.
Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. Quickly detecting relevant program invariants. In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, June 2000.
Extended Static Checking home page, Compaq Systems Research Center. On the Web at http://www.research.compaq.com/SRC/esc/.
Cormac Flanagan. Effective Static Debugging via Componential Set-Based Analysis. PhD thesis, Rice University, Houston, Texas, May 1997.
Cormac Flanagan and Steven N. Freund. Type-based race detection for Java. In Proceedings of the 2000 ACM SIGPLAN conference on Programming Design and Implementation (PLDI), pages 219–232, 2000.
Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino. Annotation inference for modular checkers. Information Processing Letters, 2001. To appear.
Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: Generating compact verification conditions. In Conference Record of the 28th Annual ACM Symposium on Principles of Programming Languages. ACM, January 2001. To appear.
S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, CAV 97: Computer Aided Verification, Lecture Notes in Computer Science 1254, pages 72–83. Springer-Verlag, 1997.
Nevin Heintze. Set-based analysis of ML programs. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 306–317, 1994.
Allan Heydon and Marc A. Najork. Mercator: A scalable, extensible web crawler. World Wide Web, 2(4):219–229, December 1999.
Java2html, Compaq Systems Research Center. On the Web at http://www.research.compaq.com/SRC/software/.
K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java users manual. Technical Note 2000-002, Compaq Systems Research Center, October 2000.
K. Rustan M. Leino, James B. Saxe, and Raymie Stata. Checking Java programs via guarded commands. In Bart Jacobs, Gary T. Leavens, Peter Müller, and Arnd Poetzsch-Heffter, editors, Formal Techniques for Java Programs, Technical Report 251. Fernuniversität Hagen, May 1999. Also available as Technical Note 1999-002, Compaq Systems Research Center, from http://www.research.compaq.com/SRC/publications/.
The Pachyderm email system, Compaq Systems Research Center. On the Web at http://www.research.compaq.com/SRC/pachyderm/, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Flanagan, C., Leino, K.R.M. (2001). Houdini, an Annotation Assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_29
Download citation
DOI: https://doi.org/10.1007/3-540-45251-6_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41791-0
Online ISBN: 978-3-540-45251-5
eBook Packages: Springer Book Archive