Junaid Haroon Siddiqui
Sarfraz Khurshid
ABSTRACT
This paper introduces a novel approach to scale symbolic execution --- a program analysis technique for systematic exploration of bounded execution paths---for test input generation. While the foundations of symbolic execution were developed over three decades ago, recent years have seen a real resurgence of the technique, specifically for systematic bug finding. However, scaling symbolic execution remains a primary technical challenge due to the inherent complexity of the path-based exploration that lies at core of the technique.
Our key insight is that the state of the analysis can be represented highly compactly: a test input is all that is needed to effectively encode the state of a symbolic execution run. We present ranged symbolic execution, which embodies this insight and uses two test inputs to define a range, i.e., the beginning and end, for a symbolic execution run. As an application of our approach, we show how it enables scalability by distributing the path exploration---both in a sequential setting with a single worker node and in a parallel setting with multiple workers. As an enabling technology, we leverage the open-source, state-of-the-art symbolic execution tool KLEE. Experimental results using 71 programs chosen from the widely deployed GNU Coreutils set of Unix utilities show that our approach provides a significant speedup over KLEE. For example, using 10 worker cores, we achieve an average speed-up of 6.6X for the 71 programs.
- V. Adve, C. Lattner, M. Brukman, A. Shukla, and B. Gaeke. LLVA: A Low-level Virtual Instruction Set Architecture. In Proc. 36th International Symposium on Microarchitecture (MICRO), pages 205--216, 2003. Google Scholar
Digital Library
- S. Anand, C. S. Pasareanu, and W. Visser. JPF-SE: a Symbolic Execution Extension to Java PathFinder. In Proc. 13th, pages 134--138, 2007. Google ScholarDigital Library
- C. Barrett and C. Tinelli. CVC3. In Proc. 19th International Conference on Computer Aided Verification (CAV), pages 298--302, 2007. Google ScholarDigital Library
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated Testing based on Java Predicates. In Proc. 2002 International Symposium on Software Testing and Analysis (ISSTA), pages 123--133, 2002. Google ScholarDigital Library
- W. R. Bush, J. D. Pincus, and D. J. Sielaff. A Static Analyzer for Finding Dynamic Programming Errors. Software Practice Experience , 30(7):775--802, June 2000. Google ScholarDigital Library
- C. Cadar and D. Engler. Execution Generated Test Cases: How to make systems code crash itself. In Proc. International SPIN Workshop on Model Checking of Software , pages 2--23, 2005. Google ScholarDigital Library
- C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically Generating Inputs of Death. In Proc. 13th Conference on Computer and Communications Security (CCS), pages 322--335, 2006. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. R. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. 8th Symposium on Operating Systems Design and Implementation (OSDI), pages 209--224, 2008. Google ScholarDigital Library
- L. A. Clarke. A System to Generate Test Data and Symbolically Execute Programs. IEEE Transactions on Software Engineering , 2(3):215-222, May 1976. Google ScholarDigital Library
- L. A. Clarke. Test Data Generation and Symbolic Execution of Programs as an aid to Program Validation. PhD thesis, University of Colorado at Boulder, 1976. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337--340, 2008. Google ScholarDigital Library
- M. B. Dwyer, S. Elbaum, S. Person, and R. Purandare. Par-allel Randomized State-Space Search. In Proc. 2007 Inter-national Conference on Software Engineering (ICSE), pages 3--12, 2007. Google ScholarDigital Library
- B. Elkarablieh, I. Garcia, Y. L. Suen, and S. Khurshid. Assertion-based Repair of Complex Data Structures. In Proc. 22nd International Conference on Automated Software Engineering (ASE), pages 64--73, 2007. Google ScholarDigital Library
- D. Funes, J. H. Siddiqui, and S. Khurshid. Ranged model checking. Under submission.Google Scholar
- P. Godefroid. Compositional Dynamic Test Generation. In Proc. Symposium on Principles of Programming Languages (POPL), pages 47--54, 2007. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In Proc. 2005 Conference on Programming Languages Design and Implementation (PLDI), pages 213--223, 2005. Google ScholarDigital Library
- P. Godefroid, M. Y. Levin, and D. A. Molnar. Automated Whitebox Fuzz Testing. In Proc. Network and Distributed System Security Symposium (NDSS), 2008.Google Scholar
- A. Grama and V. Kumar. State of the Art in Parallel Search Techniques for Discrete Optimization Problems. IEEE Transactions on Knowledge and Data Engineering , 11(1):28--35, Jan. 1999. Google ScholarDigital Library
- G. J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering , 23(5):279-295, May 1997. Google ScholarDigital Library
- V. K. Janakiram, D. P. Agrawal, and R. Mehrotra. ARandom-ized Parallel Backtracking Algorithm. IEEE Transactions on Computers, 37(12):1665--1676, Dec. 1988. Google ScholarDigital Library
- M. D. Jones and J. Sorber. Parallel Search for LTL Violations. International Journal Software Tools Technology Transfer , 7 (1):31--42, Feb. 2005. Google ScholarDigital Library
- R. M. Karp and Y. Zhang. Randomized Parallel Algorithms for Backtrack Search and Branch-and-bound Computation. Journal of the ACM, 40(3):765--789, July 1993. Google ScholarDigital Library
- S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized Symbolic Execution for Model Checking and Testing. In Proc. 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 553--568, 2003. Google ScholarDigital Library
- J. C. King. Symbolic Execution and Program Testing. Communications ACM, 19(7):385--394, July 1976. Google ScholarDigital Library
- R. Kumar and E. G. Mercer. Load Balancing Parallel Explicit State Model Checking. Electronics Notes Theory Computer Science , 128(3):19--34, Apr. 2005.Google ScholarDigital Library
- F. Lerda and R. Sisto. Distributed-Memory Model Checking with SPIN. In Proc. 5th International SPIN Workshop on Model Checking of Software , pages 22--39, 1999. Google ScholarDigital Library
- F. Lerda and W. Visser. Addressing Dynamic Issues of Program Model Checking. In Proc. 8th International SPIN Workshop on Model Checking of Software, pages 80--102, 2001. Google ScholarDigital Library
- R. Majumdar and K. Sen. Hybrid Concolic Testing. In Proc. 29th International Conference on Software Engineering (ICSE), pages 416--426, 2007. Google ScholarDigital Library
- S. Misailovic, A. Milicevic, N. Petrovic, S. Khurshid, and D. Marinov. Parallel Test Generation and Execution with Korat. In Proc. 6th joint meeting of the European Software Engineering Conference and Symposium on Foundations of Software Engineering (ESEC/FSE), pages 135--144, 2007. Google ScholarDigital Library
- R. Palmer and G. Gopalakrishnan. A Distributed Partial Order Reduction Algorithm. In Proc. 22nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), page 370, 2002. Google ScholarDigital Library
- S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed Incremental Symbolic Execution. In Proc. 2011 Conference on Programming Languages Design and Implementation (PLDI), pages 504--515, 2011. Google ScholarDigital Library
- D. A. Ramos and D. R. Engler. Practical, Low-Effort Equivalence Verification of Real Code. In Proc. 23rd International Conference on Computer Aided Verification (CAV), pages 669--685, 2011. Google ScholarDigital Library
- {33} R. Sasnauskas, O. Landsiedel, M. H. Alizai, C. Weise, S. Kowalewski, and K. Wehrle. KleeNet: Discovering Insidious Interaction Bugs in Wireless Sensor Networks Before Deployment. In Proc. 9th International Conference on Information Processing in Sensor Networks (ISPN 2010), pages 186--196, 2010. Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. CUTE: A Concolic Unit Testing Engine for C. In Proc. 5th joint meeting of the European Software Engineering Conference and Symposium on Foundations of Software Engineering (ESEC/FSE), pages 263--272, 2005. Google ScholarDigital Library
- C. Seo, S. Malek, and N. Medvidovic. Component-Level Energy Consumption Estimation for Distributed Java-Based Software Systems. In Proc. 11th International Symposium on Component-Based Software Engineering, pages 97--113, 2008. Google ScholarDigital Library
- J. H. Siddiqui and S. Khurshid. PKorat: Parallel Generation of Structurally Complex Test Inputs. In Proc. 2nd International Conference on Software Testing Verification and Validation (ICST), pages 250--259, 2009. Google ScholarDigital Library
- J. H. Siddiqui and S. Khurshid. ParSym: Parallel Symbolic Execution. In Proc. 2nd International Conference on Software Technology and Engineering (ICSTE), pages V1: 405--409, 2010.Google ScholarCross Ref
- J. H. Siddiqui and S. Khurshid. Staged Symbolic Execution. In Proc. Symposium on Applied Computing (SAC): Software Verification and Testing Track (SVT), 2012. Google ScholarDigital Library
- M. Snir and S. Otto. MPI-The Complete Reference: The MPI Core. MIT Press, 1998. Google ScholarDigital Library
- N. Sorensson and N. Een. An Extensible SAT-solver. In Proc. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 502--518, 2003.Google Scholar
- M. Staats and C. Pasareanu. Parallel Symbolic Execution for Structural Test Generation. In Proc. 19th International Symposium on Software Testing and Analysis (ISSTA), pages 183--194, 2010. Google ScholarDigital Library
- U. Stern and D. L. Dill. Parallelizing the Murphi Verifier. In Proc. 9th International Conference on Computer Aided Verification, pages 256--278, 1997. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, S. P. Park, and F. Lerda. Model Checking Programs. Automated Software Engineering Journal , 10(2):203--232, Apr. 2003. Google ScholarDigital Library
- G. Yang, C. Pasareanu, and S. Khurshid. Memoized symbolic execution. In Proc. International Symposium on Software Testing and Analysis (ISSTA), pages 144--154, 2012. Google ScholarDigital Library
Index Terms
- Scaling symbolic execution using ranged analysis
Recommendations
Scaling symbolic execution using ranged analysis
OOPSLA '12This paper introduces a novel approach to scale symbolic execution --- a program analysis technique for systematic exploration of bounded execution paths---for test input generation. While the foundations of symbolic execution were developed over three ...
Running symbolic execution forever
ISSTA 2020: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and AnalysisWhen symbolic execution is used to analyse real-world applications, it often consumes all available memory in a relatively short amount of time, sometimes making it impossible to analyse an application for an extended period. In this paper, we present a ...
Scaling symbolic execution using staged analysis
Recent advances in constraint solving technology and raw computation power have led to a substantial increase in the effectiveness of techniques based on symbolic execution for systematic bug finding. However, scaling symbolic execution remains a ...
Comments