Invariant inference for static checking:

ABSTRACT

Static checking can verify the absence of errors in a program, but often requires written annotations or specifications. As a result, static checking can be difficult to use effectively: it can be difficult to determine a specification and tedious to annotate programs. Automated tools that aid the annotation process can decrease the cost of static checking and enable it to be more widely used.This paper describes an evaluation of the effectiveness of two techniques, one static and one dynamic, to assist the annotation process. We quantitatively and qualitatively evaluate 41 programmers using ESC/Java in a program verification task over three small programs, using Houdini for static inference and Daikon for dynamic inference. We also investigate the effect of unsoundness in the dynamic analysis.Statistically significant results show that both inference tools improve task completion; Daikon enables users to express more correct invariants; unsoundness of the dynamic analysis is little hindrance to users; and users imperfectly exploit Houdini. Interviews indicate that beginning users found Daikon to be helpful; Houdini to be neutral; static checking to be of potential practical use; and both assistance tools to have unique benefits.Our observations not only provide a critical evaluation of these two techniques, but also highlight important considerations for creating future assistance tools.

REFERENCES

• 1: Nikolaj Bjørner , Anca Browne , Zohar Manna, Automatic generation of invariants and intermediate assertions, Theoretical Computer Science, v.173 n.1, p.49-87, Feb. 1997 [doi>10.1016/S0304-3975(96)00191-0]
• 2: Saddek Bensalem , Yassine Lakhnech , Hassen Saïdi, Powerful Techniques for the Automatic Generation of Invariants, Proceedings of the 8th International Conference on Computer Aided Verification, p.323-335, August 03, 1996
• 3: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• 4: David L. Detlefs. An overview of the Extended Static Checking system. In Proceedings of the First Workshop on Formal Methods in Software Practice, pages 1--9, January 1996.
• 5: David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, December 18, 1998.
• 6: Michael D. Ernst , Adam Czeisler , William G. Griswold , David Notkin, Quickly detecting relevant program invariants, Proceedings of the 22nd international conference on Software engineering, p.449-458, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337240]
• 7: 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]
• 8: 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
• 9: Bernard Elspas. The semiautomatic generation of inductive assertions for proving program correctness. Interim Report Project 2686, Stanford Research Institute, Menlo Park, CA, July 1974.
• 10: 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]
• 11: 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
• 12: 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
• 13: Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, Boston, 1999.
• 14: Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06m, Iowa State University, Department of Computer Science, February 2000. See www.cs.iastate.edu/ leavens/JML.html.
• 15: K. Rustan M. Leino , Greg Nelson, An Extended Static Checker for Modular-3, Proceedings of the 7th International Conference on Compiler Construction, p.302-305, March 28-April 04, 1998
• 16: James H. Morris, Jr. , Ben Wegbreit, Subgoal induction, Communications of the ACM, v.20 n.4, p.209-222, April 1977 [doi>10.1145/359461.359466]
• 17: Gleb Naumovich , Lori A. Clarke , Leon J. Osterweil , Matthew B. Dwyer, Verification of concurrent software with FLAVERS, Proceedings of the 19th international conference on Software engineering, p.594-595, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253489]
• 18: Jeremy W. Nimmer , Michael D. Ernst, Automatic generation of program specifications, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 19: Jeremy W. Nimmer. Automatic generation and checking of program specifications. Technical Report 852, MIT Lab for Computer Science, June 10, 2002. revision of author's Master's thesis.
• 20: Frank Pfenning. Dependent types in logic programming. In Frank Pfenning, editor, Types in Logic Programming, chapter 10, pages 285--311. MIT Press, Cambridge, MA, 1992.
• 21: Jussi Rintanen, An Iterative Algorithm for Synthesizing Invariants, Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, p.806-811, July 30-August 03, 2000
• 22: T. A. Ryan. Multiple comparisons in psychological research. Psychological Bulletin, 56:26--47, 1959.
• 23: Gerard. Salton, Automatic Information Organization and Retrieval., McGraw Hill Text, 1968
• 24: C. J. Van Rijsbergen, Information Retrieval, Butterworth-Heinemann, Newton, MA, 1979
• 25: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]
• 26: Mark Allen Weiss. Data Structures and Algorithm Analysis in Java. Addison Wesley Longman, 1999.
• 27: Ben Wegbreit , Jay M. Spitzen, Proving Properties of Complex Data Structures, Journal of the ACM (JACM), v.23 n.2, p.389-396, April 1976 [doi>10.1145/321941.321957]

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Documentation, Experimentation, Verification