RWset: Attacking Path Explosion in Constraint-Based Test Generation

  • Peter Boonstoppel
  • Cristian Cadar
  • Dawson Engler
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


Recent work has used variations of symbolic execution to automatically generate high-coverage test inputs [3, 4, 7, 8, 14]. Such tools have demonstrated their ability to find very subtle errors. However, one challenge they all face is how to effectively handle the exponential number of paths in checked code. This paper presents a new technique for reducing the number of traversed code paths by discarding those that must have side-effects identical to some previously explored path. Our results on a mix of open source applications and device drivers show that this (sound) optimization reduces the numbers of paths traversed by several orders of magnitude, often achieving program coverage far out of reach for a standard constraint-based execution system.


Model Check Base Version Symbolic Execution Device Driver Concrete State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys (April 2006)Google Scholar
  2. 2.
    Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Cadar, C., Engler, D.: Execution generated test cases: How to make systems code crash itself. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 2–23. Springer, Heidelberg (2005)Google Scholar
  4. 4.
    Cadar, C., Ganesh, V., Pawlowski, P., Dill, D., Engler, D.: EXE: Automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security (October-November 2006)Google Scholar
  5. 5.
    Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, New York (1996)Google Scholar
  7. 7.
    Godefroid, P.: Compositional dynamic test generation. In: Proceedings of the 34th Symposium on Principles of Programming Languages (POPL 2007) (January 2007)Google Scholar
  8. 8.
    Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proceedings of the Conference on Programming Language Design and Implementation (PLDI), Chicago, IL USA, ACM Press, New York (June 2005)Google Scholar
  9. 9.
    Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses (2002)Google Scholar
  10. 10.
    Herder, J.N.: Towards a true microkernel operating system. Master’s thesis, Vrije Universiteit Amsterdam (2005)Google Scholar
  11. 11.
    Holzmann, G.J.: The engineering of a model checker: The Gnu i-protocol case study revisited (1999)Google Scholar
  12. 12.
    Lewis, M., Jones, M.: A dead variable analysis for explicit model checking. In: In Proceedings of the ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program (2006)Google Scholar
  13. 13.
    Majumdar, R., Sen, K.: Hybrid concolic testing. In: Proceedings of the 29th International Conference on Software Engineering (ICSE 2007) (May 2007)Google Scholar
  14. 14.
    Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: In 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2005) (September 2005)Google Scholar
  15. 15.
    Swift, M.M., Annamalai, M., Bershad, B.N., Levy, H.M.: Recovering device drivers. In: OSDI, pp. 1–16 (December 2004)Google Scholar
  16. 16.
    Tanenbaum, A.S., Woodhull, A.S.: Operating Systems Design and Implementation, 3rd edn. Prentice Hall, Englewood Cliffs (2006)Google Scholar
  17. 17.
    Stern, U., Dill, D.L.: Improved Probabilistic Verification by Hash Compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995)Google Scholar
  18. 18.
    Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors (December 2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Peter Boonstoppel
    • 1
  • Cristian Cadar
    • 1
  • Dawson Engler
    • 1
  1. 1.Computer Systems LaboratoryStanford University 

Personalised recommendations