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.
- {BBM97} Nicolaj Bjørner, Anca Browne, and Zohar Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49-87, February 1997.]] Google ScholarDigital Library
- {BLS96} Saddek Bensalem, Yassine Lakhnech, and Hassen Saidi. Powerful techniques for the automatic generation of invariants. In CAV, pages 323-335, July 31-August 3, 1996.]] Google ScholarDigital Library
- {DC94} Matthew B. Dwyer and Lori A. Clarke. Data flow analysis for verifying properties of concurrent programs. In FSE, pages 62-75, December 1994.]] Google ScholarDigital Library
- {Det96} 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.]]Google Scholar
- {DLNS98} 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.]]Google Scholar
- {ECGN00} Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. Quickly detecting relevant program invariants. In ICSE, pages 449-458, June 2000.]] Google ScholarDigital Library
- {ECGN01} Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE TSE, 27(2):1-25, February 2001. A previous version appeared in ICSE, pages 213-224, Los Angeles, CA, USA, May 1999.]] Google ScholarDigital Library
- {EGHT94} David Evans, John Guttag, James Horning, and Yang Meng Tan. LCLint: A tool for using specifications to check code. In FSE, pages 87-97, December 1994.]] Google ScholarDigital Library
- {Els74} Bernard Elspas. The semiautomatic generation of inductive assertions for proving program correctness. Interim Report Project 2686, Stanford Research Institute, Menlo Park, CA, July 1974.]]Google Scholar
- {FJL01} Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino. Annotation inference for modular checkers. Information Processing Letters, 2(4):97-108, February 2001.]] Google ScholarDigital Library
- {FL01} Cormac Flanagan and K. Rustan M. Leino. Houdini, an annotation assistant for ESC/Java. In Formal Methods Europe, volume 2021 of LNCS, pages 500-517, Berlin, Germany, March 2001.]] Google ScholarDigital Library
- {FS01} Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: Generating compact verification conditions. In POPL, pages 193-205, January 17-19, 2001.]] Google ScholarDigital Library
- {LBR99} 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.]]Google ScholarCross Ref
- {LBR00} 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.]]Google Scholar
- {LN98} K. Rustan M. Leino and Greg Nelson. An extended static checker for Modula-3. In Compiler Construction '98, pages 302-305, April 1998.]] Google ScholarDigital Library
- {MW77} James H. Morris, Jr. and Ben Wegbreit. Subgoal induction. Communications of the ACM, 20(4):209-222, April 1977.]] Google ScholarDigital Library
- {NCOD97} Gleb Naumovich, Lori A. Clarke, Leon J. Osterweil, and Matthew B. Dwyer. Verification of concurrent software with FLAVERS. In ICSE, pages 594-595, May 1997.]] Google ScholarDigital Library
- {NE02} Jeremy W. Nimmer and Michael D. Ernst. Automatic generation of program specifications. In ISSTA, pages 232-242, July 2002.]]Google Scholar
- {Nim02} 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.]]Google Scholar
- {Pfe92} 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.]]Google Scholar
- {Rin00} Jussi Rintanen. An iterative algorithm for synthesizing invariants. In AAAI/IAAI, pages 806-811, Austin, TX, July 30-August 3, 2000.]] Google ScholarDigital Library
- {Rya59} T. A. Ryan. Multiple comparisons in psychological research. Psychological Bulletin, 56:26-47, 1959.]]Google ScholarCross Ref
- {Sal68} Gerard Salton. Automatic Information Organization and Retrieval. McGraw-Hill, 1968.]] Google ScholarDigital Library
- {vR79} C. J. van Rijsbergen. Information Retrieval. Butterworths, London, second edition, 1979.]] Google ScholarDigital Library
- {Weg74} Ben Wegbreit. The synthesis of loop predicates. Communications of the ACM, 17(2):102-112, February 1974.]] Google ScholarDigital Library
- {Wei99} Mark Allen Weiss. Data Structures and Algorithm Analysis in Java. Addison Wesley Longman, 1999.]]Google ScholarDigital Library
- {WS76} Ben Wegbreit and Jay M. Spitzen. Proving properties of complex data structures. Journal of the ACM, 23(2):389-396, April 1976.]] Google ScholarDigital Library
Index Terms
- Invariant inference for static checking: an empirical evaluation
Recommendations
Invariant inference for static checking:
SIGSOFT '02/FSE-10: Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineeringStatic 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 ...
From invariant checking to invariant inference using randomized search
We describe a general framework c2i for generating an invariant inference procedure from an invariant checking procedure. Given a checker and a language of possible invariants, c2i generates an inference procedure that iteratively invokes two phases. ...
Static contract checking with abstract interpretation
FoVeOOS'10: Proceedings of the 2010 international conference on Formal verification of object-oriented softwareWe present an overview of Clousot, our current tool to statically check CodeContracts. CodeContracts enable a compiler and language-independent specification of Contracts (precondition, postconditions and object invariants).
Clousot checks every method ...
Comments