Efficient software model checking of data structure properties

ABSTRACT

This paper presents novel language and analysis techniques that significantly speed up software model checking of data structure properties. Consider checking a red-black tree implementation. Traditional software model checkers systematically generate all red-black tree states (within some given bounds) and check every red-black tree operation (such as insert, delete, or lookup) on every red-black tree state. Our key idea is as follows. As our checker checks a red-black tree operation o on a red-black tree state s, it uses program analysis techniques to identify other red-black tree states s'₁, s'₂, ..., s'_k on which the operation o behaves similarly. Our analyses guarantee that if o executes correctly on s, then o will execute correctly on every s'_i. Our checker therefore does not need to check o on any s'_i once it checks o on s. It thus safely prunes those state transitions from its search space, while still achieving complete test coverage within the bounded domain. Our preliminary results show orders of magnitude improvement over previous approaches. We believe our techniques can make model checking significantly faster, and thus enable checking of much larger programs and complex program properties than currently possible.

REFERENCES

• 1: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 2: 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
• 3: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 4: 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
• 5: Juei Chang , Debra J. Richardson, Structural specification-based testing: automated support and experimental evaluation, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.285-302, September 06-10, 1999, Toulouse, France
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: 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]
• 8: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 9: Claudio DeMartini , Radu Iosif , Riccardo Sisto, A deadlock detection tool for concurrent Java programs, Software—Practice & Experience, v.29 n.7, p.577-603, June 1999 [doi>10.1002/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V]
• 10: Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
• 11: Daisy file system. Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software. http://-research.microsoft.com/~qadeer/cav-issta.htm.
• 12: M. Dwyer, J. Hatcliff, M. Hoosier, and Robby. Building your own software model checker using the Bogor extensible model checking framework. In Computer Aided Verification (CAV), January 2005.
• 13: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 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: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 16: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 17: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 18: J. Goodenough and S. Gerhart. Toward a theory of test data selection. IEEE Transactions on Software Engineering (TSE) SE-1(2), June 1975.
• 19: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 20: W. Grieskamp, N. Tillmann, and W. Shulte. XRT - Exploring runtime for .NET: Architecture and applications. In Workshop on Software Model Checking (SoftMC), July 2005.
• 21: 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
• 22: 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]
• 23: Hans-Martin Hörcher, Improving Software Tests Using Z Specifications, Proceedings of the 9th International Conference of Z Usres on The Z Formal Specification Notation, p.152-166, September 07-09, 1995
• 24: Radu Iosif, Symmetry Reduction Criteria for Software Model Checking, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.22-41, April 11-13, 2002
• 25: C. Norris Ip , David L. Dill, Better Verification Through Symmetry, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.97-111, April 26-28, 1993
• 26: Daniel Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.2, p.256-290, April 2002 [doi>10.1145/505145.505149]
• 27: S. Khurshid and D. Marinov. TestEra: Specification-based testing of Java programs using SAT. In Automated Software Engineering (ASE), November 2001.
• 28: S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2003.
• 29: B. Korel , J. Laski, Dynamic program slicing, Information Processing Letters, v.29 n.3, p.155-163, October 26, 1988 [doi>10.1016/0020-0190(88)90054-3]
• 30: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University, May 1998.
• 31: J. Lind-Nielsen. BuDDy. http://-sourceforge.net-/projects-/buddy.
• 32: Barbara Liskov , John Guttag, Abstraction and specification in program development, MIT Press, Cambridge, MA, 1986
• 33: Darko Marinov , Martin C. Rinard, Automatic testing of software with structurally complex inputs, Massachusetts Institute of Technology, Cambridge, MA, 2005
• 34: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 35: S. McPeak and G. C. Necula. Data structure specification via local equality axioms. In Computer Aided Verification (CAV), January 2005.
• 36: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 37: M. Musuvathi and D. Dill. An incremental heap canonicalization algorithm. In SPIN workshop on Model Checking of Software (SPIN), August 2005.
• 38: M. Musuvathi and D. R. Engler. Using model checking to find serious file system errors. In Operating System Design and Implementation (OSDI), December 2004. Winner of the best paper award.
• 39: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 40: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 41: N. Nystrom, M. R. Clarkson, and A. C. Myers. Polyglot: An extensible compiler framework for Java. In Compiler Construction (CC), April 2003.
• 42: J. Offutt and A. Abdurazik. Generating tests from UML specification. In International Conference on the Unified Modeling Language, October 1999.
• 43: Willem Visser , Corina S. Păsăreanu , Radek Pelánek, Test input generation for red-black trees using abstraction, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101983]
• 44: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 45: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 46: D. Suwimonteerabuth, S. Schwoon, and J. Esparza. jMoped: A Java bytecode checker based on Moped. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2005.
• 47: M. Vaziri and D. Jackson. Checking properties of heap-manipulating procedures using a constraint solver. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2003.
• 48: 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
• 49: Willem Visser , Corina S. Pǎsǎreanu , Sarfraz Khurshid, Test input generation with java PathFinder, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 50: J. Whaley. JavaBDD. http://-javabdd.sourceforge.net/.
• 51: Tao Xie , Darko Marinov , David Notkin, Rostra: A Framework for Detecting Redundant Object-Oriented Unit Tests, Proceedings of the 19th IEEE international conference on Automated software engineering, p.196-205, September 20-24, 2004 [doi>10.1109/ASE.2004.61]
• 52: T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), April 2005.
• 53: Xiangyu Zhang , Rajiv Gupta, Cost effective dynamic program slicing, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

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

General Terms:
Languages, Reliability, Verification

Keywords:
program analysis, software model checking