Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
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)
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)
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)
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)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, New York (1996)
Godefroid, P.: Compositional dynamic test generation. In: Proceedings of the 34th Symposium on Principles of Programming Languages (POPL 2007) (January 2007)
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)
Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses (2002)
Herder, J.N.: Towards a true microkernel operating system. Master’s thesis, Vrije Universiteit Amsterdam (2005)
Holzmann, G.J.: The engineering of a model checker: The Gnu i-protocol case study revisited (1999)
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)
Majumdar, R., Sen, K.: Hybrid concolic testing. In: Proceedings of the 29th International Conference on Software Engineering (ICSE 2007) (May 2007)
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)
Swift, M.M., Annamalai, M., Bershad, B.N., Levy, H.M.: Recovering device drivers. In: OSDI, pp. 1–16 (December 2004)
Tanenbaum, A.S., Woodhull, A.S.: Operating Systems Design and Implementation, 3rd edn. Prentice Hall, Englewood Cliffs (2006)
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)
Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors (December 2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boonstoppel, P., Cadar, C., Engler, D. (2008). RWset: Attacking Path Explosion in Constraint-Based Test Generation. In: Ramakrishnan, C.R., Rehof, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Science, vol 4963. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78800-3_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-78800-3_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78799-0
Online ISBN: 978-3-540-78800-3
eBook Packages: Computer ScienceComputer Science (R0)