Efficient solving of structural constraints

ABSTRACT

Structural constraint solving is being increasingly used for software reliability tasks such as systematic testing or error recovery. For example, the Korat algorithm provides constraint-based test generation: given a Java predicate that describes desired input constraints and a bound on the input size, Korat systematically searches the bounded input space of the predicate to generate all inputs that satisfy the constraints. As another example, the STARC tool uses a constraint-based search to repair broken data structures. A key issue for these approaches is the efficiency of search.

This paper presents a novel approach that significantly improves the efficiency of structural constraint solvers. Specifically, most existing approaches use backtracking through code re-execution to explore their search space. In contrast, our approach performs checkpoint-based backtracking by storing partial program states and performing abstract undo operations. The heart of our approach is a light-weight search that is performed purely through code instrumentation. The experimental results on Korat and STARC for generating and repairing a set of complex data structures show an order to two orders of magnitude speed-up over the traditionally used searches.

REFERENCES

• 1: 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
• 2: C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself. In Proc. 12th SPIN Workshop on Software Model Checking, 2005.
• 3: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 4: L. A. Clarke, A System to Generate Test Data and Symbolically Execute Programs, IEEE Transactions on Software Engineering, v.2 n.3, p.215-222, May 1976 [doi>10.1109/TSE.1976.233817]
• 5: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 6: Brian Demsky , Martin Rinard, Automatic detection and repair of errors in data structures, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 7: Bassem Elkarablieh , Ivan Garcia , Yuk Lai Suen , Sarfraz Khurshid, Assertion-based repair of complex data structures, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321643]
• 8: Bassem Elkarablieh , Sarfraz Khurshid , Duy Vu , Kathryn S. McKinley, Starc: static analysis for efficient repair of complex data, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 9: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 10: 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]
• 11: 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
• 12: 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]
• 13: S. Khurshid, I. García, and Y. L. Suen. Repairing structurally complex data. In Proc. 12th SPIN Workshop on Software Model Checking, 2005.
• 14: S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland, April 2003.
• 15: Sarfraz Khurshid , Yuk Lai Suen, Generalizing symbolic execution to library classes, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
• 16: J. L. Kim , T. Park, An Efficient Protocol for Checkpointing Recovery in Distributed Systems, IEEE Transactions on Parallel and Distributed Systems, v.4 n.8, p.955-960, August 1993 [doi>10.1109/71.238629]
• 17: 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]
• 18: Flavio Lerda , Willem Visser, Addressing dynamic issues of program model checking, Proceedings of the 8th international SPIN workshop on Model checking of software, p.80-102, May 2001, Toronto, Ontario, Canada
• 19: Barbara Liskov , John Guttag, Program Development in Java: Abstraction, Specification, and Object-Oriented Design, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 20: Darko Marinov , Martin C. Rinard, Automatic testing of software with structurally complex inputs, Massachusetts Institute of Technology, Cambridge, MA, 2005
• 21: 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
• 22: Sasa Misailovic , Aleksandar Milicevic , Nemanja Petrovic , Sarfraz Khurshid , Darko Marinov, Parallel test generation and execution with Korat, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287645]
• 23: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 24: 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
• 25: K. Stobie. Advanced modeling, model based test generation, and Abstract state machine Language (AsmL). Seattle Area Software Quality Assurance Group, http://www.sasqag.org/pastmeetings/asml.ppt, Jan. 2003.
• 26: Kevin Sullivan , Jinlin Yang , David Coppit , Sarfraz Khurshid , Daniel Jackson, Software assurance by bounded exhaustive testing, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 27: 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
• 28: 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
• 29: 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]
• 30: Willem Visser , Corina S. Pǎsǎreanu , Radek Pelánek, Test input generation for java containers using state matching, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146243]
• 31: Guoqing Xu , Atanas Rountev , Yan Tang , Feng Qin, Efficient checkpointing of java software using context-sensitive capture and replay, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287638]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

General Terms:
Algorithms, Reliability

Keywords:
backtracking, model checking, systematic testing