Soundness and completeness warnings in ESC/Java2

ABSTRACT

Usability is a key concern in the development of verification tools. In this paper, we present an usability extension for the verification tool ESC/Java2. This enhancement is not achieved through extensions to the underlying logic or calculi of ESC/Java2, but instead we focus on its human interface facets. User awareness of the soundness and completeness of the tool is vitally important in the verification process, and lack of information about such is one of the most requested features from ESC/Java2 users, and a primary complaint from ESC/Java2 critics. Areas of unsoundness and incompleteness of ESC/Java2 exist at three levels: the level of the underlying logic; the level of translation of program constructs into verification conditions; and at the level of the theorem prover. The user must be made aware of these issues for each particular part of the source code analysed in order to have confidence in the verification process. Our extension to ESC/Java2 provides clear warnings to the user when unsound or incomplete reasoning may be taking place.

REFERENCES

• 1: Alessandro Armando , Silvio Ranise , Michaël Rusinowitch, A rewriting approach to satisfiability procedures, Information and Computation, v.183 n.2, p.140-164, 15 June 2003 [doi>10.1016/S0890-5401(03)00020-8]
• 2: Clark Barrett and Sergey Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Rajeev Alur and Doron A. Peled, editors, CAV, Lecture Notes in Computer Science. Springer-Verlag, 2004.
• 3: Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
• 4: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 5: G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant User's Guide. INRIA, Rocquencourt, France, rapport techniques 154 edition, 1993.
• 6: Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast decision procedures. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts), volume 3114 of Lecture Notes in Computer Science, pages 175--188. Springer-Verlag, 2004.
• 7: Joseph R. Kiniry and David R. Cok. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an Internet voting tally system. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices: International Workshop, CASSIS 2004, volume 3362 of Lecture Notes in Computer Science. Springer-Verlag, Jan 2005.
• 8: Donald E. Knuth, Literate programming, Center for the Study of Language and Information, Stanford, CA, 1992
• 9: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 10: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 11: SMT-LIB: The satisfiability modulo theories library. http://goedel.cs.uiowa.edu/smtlib/.

INDEX TERMS

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

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

Keywords:
JML, completeness, extended static checking, java modeling language, soundness