Generalizing symbolic execution to library classes

ABSTRACT

Forward symbolic execution is a program analysis technique that allows using symbolic inputs to explore program executions. The traditional applications of this technique have focused on programs that manipulate primitive data types, such as integer or boolean. Recent extensions have shown how to handle reference types at their representation level. The extensions have favorably been backed by advances in constraint solving technology, and together they have made symbolic execution applicable, at least in theory, to a large class of programs. In practice, however, the increased potential for applications has created significant issues with scalability of symbolic execution to programs of non-trivial size---the ensuing path conditions rapidly become unfeasibly complex.We present Dianju, a new technique that aims to address the scalability of symbolic execution. The fundamental idea in Dianju is to perform symbolic execution of commonly used library classes (such as strings, sets and maps) at the abstract level rather than the representation level. Dianju defines semantics of operations on symbolic objects of these classes, which allows Dianju to abstract away from the complexity that is normally inherent in library implementations, thus promising scalable analyses based on symbolic execution.

REFERENCES

• 1: SGLIB---A Simple Generic Library for C. http://xref-tech.com/sglib/main.html.
• 2: T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In 16th International Conference on Computer Aided Verification (CAV), Boston, MA, July 2004.
• 3: Cyrille Artho , Howard Barringer , Allen Goldberg , Klaus Havelund , Sarfraz Khurshid , Mike Lowry , Corina Pasareanu , Grigore Rosu , Koushik Sen , Willem Visser , Rich Washington, Combining test case generation and runtime verification, Theoretical Computer Science, v.336 n.2-3, p.209-234, 26 May 2005 [doi>10.1016/j.tcs.2004.11.007]
• 4: Clark Barrett and Sergey Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Proceedings of the 16th International Conference On Computer Aided Verification, Boston, MA, July 2004.
• 5: Kent Beck and Erich Gamma. Test infected: Programmers love writing tests. Java Report, 3(7), July 1998.
• 6: 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
• 7: Robert S. Boyer , Bernard Elspas , Karl N. Levitt, SELECT—a formal system for testing and debugging programs by symbolic execution, Proceedings of the international conference on Reliable software, p.234-245, April 21-23, 1975, Los Angeles, California
• 8: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H ]
• 9: Cadence. Components of a complete assertion-based verification solution, 2005. http://www.cadence.com/whitepapers/abv_wp.pdf.
• 10: Shigeru Chiba. Javassist---a reflection-based programming wizard for Java. In Proceedings of the ACM OOPSLA '98 Workshop on Reflective Programming in C++ and Java, October 1998.
• 11: Christoph Csallner , Yannis Smaragdakis, Check 'n' crash: combining static checking and testing, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062533]
• 12: Markus Dahm. Byte code engineering library. http://bcel.sourceforge.net/.
• 13: 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
• 14: Iván García. Enabling symbolic execution of Java programs using bytecode instrumentation. Master's thesis, Department of Electrical and Computer Engineering, The University of Texas at Austin, May 2005.
• 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 , Nils Klarlund , Koushik Sen, DART: directed automated random testing, ACM SIGPLAN Notices, v.40 n.6, June 2005
• 17: 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 ]
• 18: Daniel Jackson. Micromodels of software: Modelling and analysis with Alloy, 2001.
• 19: Sarfraz Khurshid, Iván García, and Yuk Lai Suen. Repairing structurally complex data. In 12th International SPIN Workshop on Model Checking of Software, San Francisco, CA, August 2005.
• 20: Sarfraz Khurshid, Corina Pasareanu, and Willem Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland, April 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: Bogdan Korel, Automated test data generation for programs with procedures, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.209-215, January 08-10, 1996, San Diego, California, United States
• 23: Barbara Liskov , B. Liskov, Program Development in Java: Abstraction, Specification, and Object-Oriented Design, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 24: Darko Marinov , Martin C. Rinard, Automatic testing of software with structurally complex inputs, Massachusetts Institute of Technology, Cambridge, MA, 2005
• 25: Darko Marinov, Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid, and Martin Rinard. An evaluation of exhaustive testing for data structures. Technical Report MIT-LCS-TR-921, MIT CSAIL, Cambridge, MA, September 2003.
• 26: 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
• 27: Corina S. Pasareanu and Willem Visser. Verification of java programs using symbolic execution and invariant generation. In Proc. 11th International SPIN Workshop on Model Checking of Software, Barcelona, Spain, April 2004.
• 28: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 29: Sanjit A. Seshia , Randal E. Bryant, Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.100-109, July 13-17, 2004
• 30: Yuk Lai Suen. Automatically repairing structurally complex data. Master's thesis, Department of Electrical and Computer Engineering, The University of Texas at Austin, May 2005.
• 31: Sun Microsystems. Java 2 Platform, Standard Edition, v1.3.1 API Specification.
• 32: Synopsis. Assertion-based verification, March 2003. http://www.synopsys.com/products/simulation/assertion_based_wp.pdf.
• 33: Margus Veanes, Colin Campbell, Wolfram Schulte, Pushmeet Kohli, N. Tillmann, and W. Grieskamp. On-the-fly testing of reactive systems. (Submitted for publication.).
• 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: 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
• 36: Srinivas Visvanathan and Neelam Gupta. Generating test data for functions with pointer inputs. Edinburgh, Scotland, September 2002.
• 37: Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th conference on Design automation, p.542-545, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379019]
• 38: Tao Xie, Darko Marinov, Wolfram Schulte, and David Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Proc. 11th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Edinburgh, UK, April 2005.

INDEX TERMS

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

Keywords:
korat, model checking, symbolic execution, test input generation