Modular verification of code with SAT

ABSTRACT

An approach is described for checking the methods of a class against a full specification. It shares with traditional model checking the idea of exhausting the entire space of executions within some finite bounds, and with traditional verification the idea of modular analysis, in which a method is analyzed, in isolation, for all possible calling contexts.The analysis involves an automatic two-phase reduction: first, to an intermediate form in relational logic (using a new encoding described here), and second, to a boolean formula (using existing techniques), which is then handed to an off the shelf SAT solver.A variety of implementations of the Java Collections Framework's List interface were checked against existing JML specifications. The analysis revealed bugs in the implementations, as well as errors in the specifications themselves.

REFERENCES

• 1: 6.170 Laboratory in Software Engineering, Fall 2001. http://www.ocw.mit.edu/OcwWeb/Electrical- Engineering-and-Computer-Science/6-170Fall- 2005/CourseHome/.
• 2: GNU Trove: High performance collections for Java. http://trove4j.sourceforge.net/.
• 3: Jakarta Commons-Collections. http://jakarta.apache.org/commons/collections/.
• 4: JML Specifications for the Java Collections Framework. http://www.cs.iastate.edu/leavens/JMLrelease/javadocs/java/util/Collection.html.
• 5: The Alloy Analyzer. http://alloy.mit.edu/.
• 6: A. Andoni, D. Daniliuc, S. Khurshid, and D. Marinov. Evaluating the "Small Scope Hypothesis". Technical Report MIT-LCS-TR-921, MIT CSAIL, 2003.
• 7: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 8: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 9: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 10: 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]
• 11: C.A.R. Hoare. Proofs of Correctness of Data Representations. Acta Informatica, 1(4), 1972.
• 12: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 13: Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri, NUSMV: A New Symbolic Model Verifier, Proceedings of the 11th International Conference on Computer Aided Verification, p.495-499, July 06-10, 1999
• 14: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 15: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 16: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 17: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 18: Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 19: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 20: Daniel Jackson, Object models as heap invariants, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
• 21: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 22: B. W. Lampson. Software Components: Only the Giants Survive. In K. S. J. Andrew Herbert, editor, Computer Systems: Papers for Roger Needham, Lecture Notes in Computer Science, pages 59--65. Springer-Verlag Berlin, 2004.
• 23: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 24: Darko Marinov , Sarfraz Khurshid, TestEra: A Novel Framework for Automated Testing of Java Programs, Proceedings of the 16th IEEE international conference on Automated software engineering, p.22, November 26-29, 2001
• 25: M. D. McIlroy. Mass-Produced Software Components. In J. M. Buxton, P. Naur, and B. Randell, editors, Software Engineering Concepts and Techniques (1968 NATO Conference of Software Engineering), pages 88--98. NATO Science Committee, Oct 1968.
• 26: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 27: Sun Microsystems. Java Collections Framework. http://java.sun.com/j2se/1.5.0/docs/guide/collections/.
• 28: Mana Taghdiri, Inferring Specifications to Detect Errors in Code, Proceedings of the 19th IEEE international conference on Automated software engineering, p.144-153, September 20-24, 2004 [doi>10.1109/ASE.2004.42]
• 29: E. Torlak and D. Jackson. The Design of a Relational Engine. Submitted for publication, 2006.
• 30: Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
• 31: 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
• 32: M. Vaziri. Finding Bugs in Software with a Constraint Solver. PhD thesis, Massachusetts Institute of Technology, MA, USA, Feb. 2004.
• 33: M. Vaziri and D. Jackson. Checking Heap-Manipulating Procedures with a Constraint Solver. In 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), 2003.
• 34: 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
• 35: Y. Xie and A. Aiken. Saturn: A SAT-Based Tool for Bug Detection. In 17th International Conference on Computer Aided Verification (CAV 2005), Edinburgh, Scotland, UK, 2005.

INDEX TERMS

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

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

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
SAT, alloy, first-order logic, formal methods, formal verification, software model checking