Finding bugs efficiently with a SAT solver

ABSTRACT

We present an approach for checking code against rich specifications, based on existing work that consists of encoding the program in a relational logic and using a constraint solver to find specification violations. We improve the efficiency of this approach with a new encoding of the program that effectively slices it at the logical level with respect to the specification. We also present new encodings for integer values and arrays, enabling the verification of realistic fragments of code that manipulate both. Our technique can handle integers of much larger ranges than previously possible, and permits large sparse arrays to be handled efficiently.

We present a soundness proof for our slicing algorithm and a general condition under which relational formulae may be sliced. We implemented our technique and evaluated it by checking data structure invariants of several classes taken from the Java Collections Framework. We also checked for violations of Java's equality contract in a variety of open-source programs, and found several bugs.

REFERENCES

• 1: Spin model checker. http://spinroot.com/spin/whatispin.html.
• 2: 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
• 3: 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
• 4: 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
• 5: 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
• 6: 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]
• 7: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 8: Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 9: Greg Dennis , Felix Sheng-Ho Chang , Daniel Jackson, Modular verification of code with SAT, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146251]
• 10: Java equals() and compareto() contracts. http://java.sun.com/j2se/1.5.0/docs/api/java/lang/package-summary.html.
• 11: 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
• 12: Grammatech, I. Codesurfer. http://www.grammatech.com/products/codesurfer/index.html.
• 13: John Hatcliff , James C. Corbett , Matthew B. Dwyer , Stefan Sokolowski , Hongjun Zheng, A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, Proceedings of the 6th International Symposium on Static Analysis, p.1-18, September 22-24, 1999
• 14: John Hatcliff , Matthew B. Dwyer , Hongjun Zheng, Slicing Software for Model Construction, Higher-Order and Symbolic Computation, v.13 n.4, p.315-353, Dec. 1, 2000 [doi>10.1023/A:1026599015809]
• 15: Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998 [doi>10.1109/32.730543]
• 16: 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
• 17: David Hovemeyer , William Pugh, Finding bugs is easy, ACM SIGPLAN Notices, v.39 n.12, December 2004 [doi>10.1145/1052883.1052895]
• 18: 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
• 19: 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
• 20: 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
• 21: Khurshid, S., Pasareanu, C., and Visser, W. Generalized symbolic execution for model checking and testing. In TACAS'03: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003).
• 22: 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
• 23: 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
• 24: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 25: Millett, L. I., and Teitelbaum, T. Slicing Promela and its applications to model checking. In Proceedings of the 4th International SPIN Workshop (1998).
• 26: 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]
• 27: Tip, F. A survey of program slicing techniques. Journal of Programming Languages 3, 3 (1995), 121--189.
• 28: Torlak, E., and Jackson, D. Kodkod: A relational model finder. In TACAS'07: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2007).
• 29: Engin Uzuncaova , Sarfraz Khurshid, Kato: A Program Slicing Tool for Declarative Specifications, Proceedings of the 29th international conference on Software Engineering, p.767-770, May 20-26, 2007 [doi>10.1109/ICSE.2007.47]
• 30: Raja Vallée-Rai , Phong Co , Etienne Gagnon , Laurie Hendren , Patrick Lam , Vijay Sundaresan, Soot - a Java bytecode optimization framework, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.13, November 08-11, 1999, Mississauga, Ontario, Canada
• 31: Vaziri, M., and Jackson, D. Checking properties of heap-manipulating procedures with a constraint solver. In TACAS'03: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003).
• 32: Vaziri, M., Tip, F., Fink, S., and Dolby, J. Declarative object identity using relation types. In ECOOP'07: Proceedings of the European Conference on Object-Oriented Programming (2007), pp. 54--78.
• 33: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 34: Watson Libraries for Analysis (WALA). http://wala.sourceforge.net/.
• 35: Yichen Xie , Alex Aiken, Saturn: A scalable framework for error detection using Boolean satisfiability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.16-es, May 2007 [doi>10.1145/1232420.1232423]

INDEX TERMS

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

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

General Terms:
Theory, Verification

Keywords:
SAT solving, model checking, slicing, specification