Marcelo d'Amorim
Steven Lauterburg
ABSTRACT
State-space exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in exploration of object-oriented programs is handling the program state, in particular the heap. Previous research has focused on standard program execution that operates on one state/heap. We present Delta Execution, a technique that simultaneously operates on several states/heaps. It exploits the fact that many execution paths in state-space exploration partially overlap and speeds up the exploration by sharing the common parts across the executions and separately executing only the "deltas" where the executions differ.
We have implemented Delta Execution in JPF, a popular general-purpose model checker for Java programs, and in BOX, a specialized model checker that we have developed for efficient exploration of sequential Java programs. We have evaluated Delta Execution for (bounded) exhaustive exploration of ten basic subject programs without errors. The experimental results show that on average Delta Execution improves the exploration time 10.97x (over an order of magnitude) in JPF and 2.07x in BOX. We have also evaluated Delta Execution for one larger case study with errors, where the exploration time improved up to 1.43x.
- T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In CAV, 2004.Google Scholar
- T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI, 2001. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN, 2000. Google ScholarDigital Library
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In ISSTA, 2002. Google ScholarDigital Library
- R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3), 1992. Google ScholarDigital Library
- C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In CCS, 2006. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, MA, 1999. Google ScholarDigital Library
- J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In ICSE, 2000. Google ScholarDigital Library
- C. Csallner and Y. Smaragdakis. JCrasher: An automatic robustness tester for Java. Software Practice and Experience, 34, 2004. Google ScholarDigital Library
- Daisy File System. Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software.Google Scholar
- M. d'Amorim, S. Lauterburg, and D. Marinov. Delta execution for efficient state-space exploration of object-oriented programs. Technical Report UIUCDCS-R-2007-2844, University of Illinois, Urbana, IL, April 2007.Google Scholar
- M. d'Amorim, C. Pacheco, T. Xie, D. Marinov, and M. D. Ernst. An empirical comparison of automated generation and classification techniques for object-oriented unit testing. In ASE, 2006. Google ScholarDigital Library
- M. d'Amorim, A. Sobeih, and D. Marinov. Optimized execution of deterministic blocks in Java PathFinder. In ICFEM, 2006. Google ScholarDigital Library
- P. T. Darga and C. Boyapati. Efficient software model checking of data structure properties. In OOPSLA, 2006. Google ScholarDigital Library
- Eclipse foundation. http://www.eclipse.org/.Google Scholar
- Foundations of Software Engineering at Microsoft Research. The AsmL test generator tool. http://research.microsoft.com/fse/AsmL.Google Scholar
- D. P. Friedman, M. Wand, and C. T. Haynes. Essentials of Programming Languages. MIT Press, 2001. Google ScholarDigital Library
- P. Godefroid. Model checking for programming languages using Verisoft. In POPL, 1997. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In PLDI, 2005. Google ScholarDigital Library
- K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4), 2000.Google Scholar
- G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5), 1997. Google ScholarDigital Library
- R. Iosif. Exploiting heap symmetries in explicit-state model checking of software. In ASE, 2001. Google ScholarDigital Library
- J-Sim. http://www.j-sim.org/.Google Scholar
- J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In LICS, 1990.Google Scholar
- S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS, April 2003.Google ScholarDigital Library
- V. Kuncak, P. Lam, and M. Rinard. Role analysis. In POPL, Jan. 2002. Google ScholarDigital Library
- F. Lerda and W. Visser. Addressing dynamic issues of program model checking. In SPIN '01, 2001. Google ScholarDigital Library
- O. Lhotak and L. Hendren. Jedd: A BDD-based relational extension of Java. In PLDI, 2004. Google ScholarDigital Library
- P. C. Mehlitz, W. Visser, and J. Penix. The JPF runtime verification system. http://javapathfinder.sourceforge.net/JPF.pdf.Google Scholar
- M. Musuvathi and D. L. Dill. An incremental heap canonicalization algorithm. In SPIN, 2005. Google ScholarDigital Library
- M. Musuvathi, D. Park, A. Chou, D. R. Engler, and D. L. Dill. CMC: A pragmatic approach to model checking real code. In OSDI, 2002. Google ScholarDigital Library
- A. J. Offutt, Z. Jin, and J. Pan. The dynamic domain reduction procedure for test data generation. Software Practice and Experience, 29(2), 1999. Google ScholarDigital Library
- C. Pacheco and M. D. Ernst. Eclat: Automatic generation and classification of test inputs. In ECOOP, 2005. Google ScholarDigital Library
- C. E. Perkins and E. M. Royer. Ad-hoc on-demand distance vector routing. In Proc. IEEE Workshop on Mobile Computing Systems and Applications (WMCSA), pages 90--100. IEEE Computer Society Press, 1999. Google ScholarDigital Library
- Robby, M. B. Dwyer, and J. Hatcliff. Bogor: An extensible and highly-modular software model checking framework. In ESEC/FSE, 2003. Google ScholarDigital Library
- R. Rugina. Quantitative shape analysis. In 11th International Static Analysis Symposium (SAS'04), Aug. 2004.Google ScholarCross Ref
- K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE, September 2005. Google ScholarDigital Library
- A. Sobeih, M. Viswanathan, D. Marinov, and J. C. Hou. Finding bugs in network protocols using simulation code and protocol-specific heuristics. In ICFEM, volume 3785 of LNCS, 2005. Google ScholarDigital Library
- D. Stotts, M. Lindsey, and A. Antley. An informal formal method for systematic JUnit test case generation. In Proc. 2002 XP/Agile Universe, 2002. Google ScholarDigital Library
- W. Visser, C. S. Pasareanu, and S. Khurshid. Test input generation with Java PathFinder. In ISSTA, 2004. Google ScholarDigital Library
- W. Visser, C. S. Pasareanu, and R. Pelanek. Test input generation for red-black trees using abstraction. In ASE, 2005. Google ScholarDigital Library
- W. Visser, C. S. Pasareanu, and R. Pelanek. Test input generation for Java containers using state matching. In ISSTA, 2006. Google ScholarDigital Library
- J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI, 2004. Google ScholarDigital Library
- T. Xie, D. Marinov, and D. Notkin. Rostra: A framework for detecting redundant object-oriented unit tests. In ASE, 2004. Google ScholarDigital Library
- T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In TACAS, 2005. Google ScholarDigital Library
- G. Yorsh, T. W. Reps, and S. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In TACAS, 2004.Google ScholarCross Ref
- Y. Zhou, D. Marinov, W. Sanders, C. Zilles, M. d'Amorim, S. Lauterburg, R. M. Lefever, and J. Tucek. Delta execution for software reliability. To appear in HotDep, 2007. Google ScholarDigital Library
Index Terms
- Delta execution for efficient state-space exploration of object-oriented programs
Recommendations
Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs
We present Delta Execution, a technique that speeds up state-space exploration of object-oriented programs. State-space exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in ...
Efficient online validation with delta execution
ASPLOS 2009Software systems are constantly changing. Patches to fix bugs and patches to add features are all too common. Every change risks breaking a previously working system. Hence administrators loathe change, and are willing to delay even critical security ...
Efficient online validation with delta execution
ASPLOS XIV: Proceedings of the 14th international conference on Architectural support for programming languages and operating systemsSoftware systems are constantly changing. Patches to fix bugs and patches to add features are all too common. Every change risks breaking a previously working system. Hence administrators loathe change, and are willing to delay even critical security ...
Comments