skip to main content
10.1145/1831708.1831732acmconferencesArticle/Chapter ViewAbstractPublication PagesisstaConference Proceedingsconference-collections
research-article

Parallel symbolic execution for structural test generation

Authors Info & Claims
Published:12 July 2010Publication History

ABSTRACT

Symbolic execution is a popular technique for automatically generating test cases achieving high structural coverage. Symbolic execution suffers from scalability issues since the number of symbolic paths that need to be explored is very large (or even infinite) for most realistic programs. To address this problem, we propose a technique, Simple Static Partitioning, for parallelizing symbolic execution. The technique uses a set of pre-conditions to partition the symbolic execution tree, allowing us to effectively distribute symbolic execution and decrease the time needed to explore the symbolic execution tree. The proposed technique requires little communication between parallel instances and is designed to work with a variety of architectures, ranging from fast multi-core machines to cloud or grid computing environments. We implement our technique in the Java PathFinder verification tool-set and evaluate it on six case studies with respect to the performance improvement when exploring a finite symbolic execution tree and performing automatic test generation.

We demonstrate speedup in both the analysis time over finite symbolic execution trees and in the time required to generate tests relative to sequential execution, with a maximum analysis time speedup of 90x observed using 128 workers and a maximum test generation speedup of 70x observed using 64 workers.

References

  1. P. E. Ammann, P. E. Black, and W. Majurski. Using model checking to generate tests from specifications. In Proc. of 2nd IEEE Int'l. Conference on Formal Engineering Methods, pages 46--54. IEEE Computer Society, Nov. 1998. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. S. Anand, C. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to Java PathFinder. In Proc. of 13th TACAS Conference, volume 4424, page 134. Springer, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. J. Barnat, L. Brim, and J. Chaloupka. Parallel breadth-first search LTL model-checking. In Proc. of 18th IEEE Int'l. Conference on Automated Software Engineering, pages 106--115, 2003.Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. B. Bezier. Software Testing Techniques, 2nd Edition. Van Nostrand Reinhold, New York, 1990. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated Testing Based on Java Predicates. In Proc. of the 2002 ACM SIGSOFT Int'l. Symposium on Software Testing and Analysis, pages 123--133. ACM New York, NY, USA, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. J. Chilenski and S. Miller. Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, 9:193--200, September 1994.Google ScholarGoogle ScholarCross RefCross Ref
  7. L. Ciortea, C. Zamfir, S. Bucur, V. Chipounov, and G. Candea. Cloud9: A Software Testing Service.Google ScholarGoogle Scholar
  8. T. Downing. Java RMI: remote method invocation. IDG Books Worldwide, Inc. Foster City, CA, USA, 1998. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. M. Dwyer, S. Elbaum, S. Person, and R. Purandare. Parallel randomized state-space search. In Proc of 29th Int'l. Conference on Software Engineering, pages 3--12, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. B. Elkarablieh, D. Marinov, and S. Khurshid. Efficient solving of structural constraints. In Proc. of the 2008 International Symposium on Software Testing and Analysis, pages 39--50. ACM New York, NY, USA, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. P. Godefroid. Compositional dynamic test generation. In Proc. of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47--54. ACM New York, NY, USA, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. G. Holzmann and D. Bosnacki. The design of a multicore extension of the spin model checker. IEEE Transactions on Software Engineering, 33(10):659--674, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. G. Holzmann, R. Joshi, and A. Croce. Tackling large verification problems with the swarm tool. Proc. 15th Int'l. SPIN Workshop, 5156:134--143, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. Proc. of the 9th TACAS, pages 553--568, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. A. King. Distributed parallel symbolic execution. Master's thesis, Kansas State University, 2009.Google ScholarGoogle Scholar
  16. J. King. Symbolic execution and program testing. "Communications of the ACM", 1976. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. C. Pǎsǎreanu, P. Mehlitz, D. Bushnell, K. Gundy Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In Proc. of the 2008 Int'l. Symposium on Software Testing and Analysis, pages 15--26. ACM New York, NY, USA, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. C. Pǎsǎreanu, J. Schumann, P. Mehlitz, G. Karsai, H. Nine, and S. Nima. Test-case generation for Simulink / Stateflow models of software-intensive mission-critical systems. In 3rd IEEE Int'l. Conference on Space Mission Challenges for Information Technology, 2009.Google ScholarGoogle Scholar
  19. C. Ramamoorthy, S. Ho, and W. Chen. On the automated generation of program test data. IEEE Transactions on Software Engineering, pages 293--300, 1976. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. S. Rayadurgam and M. P. Heimdahl. Coverage based test-case generation using model checkers. In Proc. of the 8th IEEE Int'l. Conference and Workshop on the Engineering of Computer Based Systems, pages 83--91. IEEE Computer Society, April 2001.Google ScholarGoogle ScholarCross RefCross Ref
  21. K. Sen and G. Agha. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. Computer Aided Verification, 4144:419, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. J. Siddiqui and S. Khurshid. Pkorat: Parallel generation of structurally complex test inputs. In Proc. of the 2009 International Conference on Software Testing Verification and Validation, pages 250--259. IEEE Computer Society Washington, DC, USA, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. M. Staats. Towards a framework for generating tests to satisfy complex code coverage in Java Pathfinder. In Proc. of NASA Formal Methods Symposium 2009, 2009.Google ScholarGoogle Scholar
  24. U. Stern and D. Dill. Parallelizing the Murφ verifier. Formal Methods in System Design, 18(2):117--129, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. J. Sztipanovits and G. Karsai. Generative programming for embedded systems. In Proc. of Int'l. Conference on Principles and Practice of Declarative Programming, volume 6, pages 180--180. Springer, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. In Proc. of Automated Software Engineering, pages 203--232. Springer, 2003. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. W. Visser, C. Pǎsǎreanu, and R. Pelánek. Test input generation for java containers using state matching. In Proc. of the 2006 Int'l. Symposium on Software Testing and Analysis, pages 37--48. ACM New York, NY, USA, 2006 Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Parallel symbolic execution for structural test generation

    Recommendations

    Comments

    Login options

    Check if you have access through your login credentials or your institution to get full access on this article.

    Sign in
    • Published in

      cover image ACM Conferences
      ISSTA '10: Proceedings of the 19th international symposium on Software testing and analysis
      July 2010
      294 pages
      ISBN:9781605588230
      DOI:10.1145/1831708

      Copyright © 2010 ACM

      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      • Published: 12 July 2010

      Permissions

      Request permissions about this article.

      Request Permissions

      Check for updates

      Qualifiers

      • research-article

      Acceptance Rates

      Overall Acceptance Rate58of213submissions,27%

    PDF Format

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader