Extended static checking for Java

ABSTRACT

Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static Checker for Java (ESC/Java), an experimental compile-time program checker that finds common programming errors. The checker is powered by verification-condition generation and automatic theorem-proving techniques. It provides programmers with a simple annotation language with which programmer design decisions can be expressed formally. ESC/Java examines the annotated software and warns of inconsistencies between the design decisions recorded in the annotations and the actual code, and also warns of potential runtime errors in the code. This paper gives an overview of the checker architecture and annotation language and describes our experience applying the checker to tens of thousands of lines of Java programs.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 2: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 3: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 4: N. Cataño and M. Huisman. Formal specification of Gemplus' electronic purse case study. In Proc. of Formal Methods Europe (FME 2002). Springer-Verlag, 2002. To Appear
• 5: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 8: D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq SRC, Dec. 1998
• 9: D. L. Detlefs, G. Nelson, and J. B. Saxe. A theorem prover for program checking. Research Report 178, Compaq SRC, 2002. In preparation
• 10: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 11: M. Dwyer, J. Hatcliff, and R. Howell. CIS 771: Software specification. Kansas State Univ., Dept. of Comp. and Inf. Sciences, Spring 2001
• 12: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 13: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st international conference on Software engineering, p.213-224, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302467]
• 14: Escher Technologies, Inc. Getting started with Perfect. Available from www.eschertech.com, 2001
• 15: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 16: Cormac Flanagan , Rajeev Joshi , K. Rustan M. Leino, Annotation inference for modular checkers, Information Processing Letters, v.77 n.2-4, p.97-108, Feb. 1, 2001 [doi>10.1016/S0020-0190(00)00196-4]
• 17: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 18: Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-202, January 16-18, 2002, Portland, Oregon
• 19: Cormac Flanagan , James B. Saxe, Avoiding exponential explosion: generating compact verification conditions, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.193-205, January 2001, London, United Kingdom
• 20: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 21: Allan Heydon , Marc Najork, Mercator: A scalable, extensible Web crawler, World Wide Web, v.2 n.4, p.219-229, 1999 [doi>10.1023/A:1019213109274]
• 22: C. A. R. Hoare. Proof of correctness of data representations. Acta Inf., 1(4):271--81, 1972
• 23: S. C. Johnson. Lint, a C program checker. Comp. Sci. Tech. Rep. 65, Bell Laboratories, 1978
• 24: B. W. Lampson, J. J. Horning, R. L. London, J. G. Mitchell, and G. J. Popek. Report on the programming language Euclid. Technical Report CSL-81-12, Xerox PARC, Oct. 1981
• 25: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06f, Dept. of Comp. Sci., Iowa State Univ., July 1999
• 26: Gary T. Leavens , Clyde Ruby , K. Rustan , M. Leino , Erik Poll , Bart Jacobs, JML (poster session): notations and tools supporting detailed design in Java, Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), p.105-106, January 2000, Minneapolis, Minnesota, United States [doi>10.1145/367845.367996]
• 27: K. R. M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. In FOOL 4, 1997
• 28: K. Rustan M. Leino, Data groups: specifying the modification of extended state, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.144-153, October 18-22, 1998, Vancouver, British Columbia, Canada
• 29: K. Rustan M. Leino, Applications of Extended Static Checking, Proceedings of the 8th International Symposium on Static Analysis, p.185-193, July 16-18, 2001
• 30: K. Rustan M. Leino, Extended Static Checking: A Ten-Year Perspective, Informatics - 10 Years Back. 10 Years Ahead., p.157-175, January 2001
• 31: K. Rustan M. Leino , Rajit Manohar, Joining specification statements, Theoretical Computer Science, v.216 n.1-2, p.375-394, March 11, 1999 [doi>10.1016/S0304-3975(98)00165-0]
• 32: K. R. M. Leino and G. Nelson. Data abstraction and information hiding. Research Report 160, Compaq SRC, Nov. 2000
• 33: K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java user's manual. Tech. Note 2000-002, Compaq SRC, Oct. 2000
• 34: K. Rustan M. Leino , Arnd Poetzsch-Heffter , Yunhong Zhou, Using data groups to specify and check side effects, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 35: K. R. M. Leino, J. B. Saxe, and R. Stata. Checking Java programs via guarded commands. In B. Jacobs et al., editor, Formal Techniques for Java Programs, Tech. Report 251. Fernuniversität Hagen, May 1999
• 36: K. R. M. Leino and R. Stata. Checking object invariants. Tech. Note 1997-007, DEC SRC, Jan. 1997
• 37: Bertrand Meyer, Object-Oriented Software Construction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• 38: T. Millstein. Toward more informative ESC/Java warning messages. In J. Mason, editor, Selected 1999 SRC summer intern reports, Tech. Note 1999-003. Compaq SRC, 1999
• 39: P. Müller, A. Poetzsch-Heffter, and G. T. Leavens. Modular specification of frame properties in JML. Technical Report 02-02, Dept. of Comp. Sci., Iowa State Univ., Feb. 2002. To appear in Concurrency, Practice and Experience
• 40: J. W. Nimmer and M. D. Ernst. Automatic generation and checking of program specifications. Technical Report 823, MIT Lab for Computer Science, Aug. 2001
• 41: Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
• 42: Erik Poll , Joachim van den Berg , Bart Jacobs, Specification of the Javacard API in JML, Proceedings of the fourth working conference on smart card research and advanced applications on Smart card research and advanced applications, p.135-154, February 2001, Bristol, United Kingdom
• 43: N. Sterling. WARLOCK --- a static data race analysis tool. In Proc. Winter 1993 USENIX Conf., pages 97--106. USENIX Assoc., Jan. 1993
• 44: M. Turin, A. Deutsch, and G. Gonthier. La verification des programmes d'ariane. Pour la Science, 243:21--22, Jan. 1998. (In French)
• 45: Joachim van den Berg , Bart Jacobs, The LOOP Compiler for Java and JML, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.299-312, April 02-06, 2001
• 46: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 47: J. M. Wing, A TWO-TIERED APPROACH TO SPECIFYING PROGRAMS, Massachusetts Institute of Technology, Cambridge, MA, 1983
• 48: J. B. Wordsworth, Software engineering with B, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 49: Hongwei Xi, Imperative Programming with Dependent Types, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.375, June 26-29, 2000
• 50: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Design, Documentation, Verification

Keywords:
compile-time program checking