research-article

Symbolic execution with mixed concrete-symbolic solving

Authors:

Corina S. Păsăreanu,

Willem VisserAuthors Info & Claims

ISSTA '11: Proceedings of the 2011 International Symposium on Software Testing and Analysis

Pages 34 - 44

https://doi.org/10.1145/2001420.2001425

Published: 17 July 2011 Publication History

Abstract

Symbolic execution is a powerful static program analysis technique that has been used for the automated generation of test inputs. Directed Automated Random Testing (DART) is a dynamic variant of symbolic execution that initially uses random values to execute a program and collects symbolic path conditions during the execution. These conditions are then used to produce new inputs to execute the program along different paths. It has been argued that DART can handle situations where classical static symbolic execution fails due to incompleteness in decision procedures and its inability to handle external library calls.

We propose here a technique that mitigates these previous limitations of classical symbolic execution. The proposed technique splits the generated path conditions into (a) constraints that can be solved by a decision procedure and (b) complex non-linear constraints with uninterpreted functions to represent external library calls. The solutions generated from the decision procedure are used to simplify the complex constraints and the resulting path conditions are checked again for satisfiability. We also present heuristics that can further improve our technique. We show how our technique can enable classical symbolic execution to cover paths that other dynamic symbolic execution approaches cannot cover. Our method has been implemented within the Symbolic PathFinder tool and has been applied to several examples, including two from the NASA domain.

References

[1]

W. Bush, J. Pincus, and D. Sielaff. A static analyzer for finding dynamic programming errors. Software: Practice and Experience, 30(7):775--802, 2000.

Digital Library

[2]

C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, pages 209--224. USENIX Association, 2008.

Digital Library

[3]

C. Cadar, V. Ganesh, P. Pawlowski, D. Dill, and D. Engler. EXE: automatically generating inputs of death. TISSEC, 12(2):1--38, 2008.

Digital Library

[4]

Choco Solver. http://www.emn.fr/z-info/choco-solver/.

[5]

L. A. Clarke. A program testing system. In Proceedings of the 1976 annual conference, ACM '76, pages 488--491, 1976.

Digital Library

[6]

A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezzé. Using symbolic execution for verifying safety-critical systems. In ESEC/FSE, page 151. ACM, 2001.

Digital Library

[7]

X. Deng, Robby, and J. Hatcliff. Kiasan/KUnit: Automatic test case generation and analysis feedback for open object-oriented systems. In TAICPART-MUTATION, pages 3--12, 2007.

Digital Library

[8]

D. Giannakopoulou, D. Bushnell, J. Schumann, H. Erzberger, and K. Heere. Formal testing for separation assurance. In To Appear, Annals of Mathematics and Artificial Intelligence. Springer, 2011.

Digital Library

[9]

P. Godefroid. Compositional dynamic test generation. In POPL, pages 47--54. ACM, 2007.

Digital Library

[10]

P. Godefroid. Higher-Order Test Generation. Proc. PLDI, 2011.

Digital Library

[11]

P. Godefroid, P. de Halleux, A. Nori, S. Rajamani, W. Schulte, N. Tillmann, and M. Levin. Automating software testing using program analysis. Software, IEEE, 25(5):30--37, 2008.

Digital Library

[12]

P. Godefroid, N. Klarlund, and K. Sen. Dart: Directed automated random testing. SIGPLAN Not., 40(6):213--223, 2005.

Digital Library

[13]

Java PathFinder Tool-set. http://babelfish.arc.nasa.gov/trac/jpf.

[14]

S. Khurshid, C. Păsăreanu, and W. Visser. Generalized symbolic execution for model checking and testing. Proc. TACAS, pages 553--568, 2003.

Digital Library

[15]

J. C. King. Symbolic execution and program testing. Comm. ACM, 19(7):385--394, 1976.

Digital Library

[16]

K. Lakhotia, N. Tillmann, M. Harman, and J. De Halleux. Flopsy: search-based floating point constraint solving for symbolic execution. In ICTSS, pages 142--157, Berlin, Heidelberg, 2010. Springer-Verlag.

Digital Library

[17]

T. Menzies and Y. Hu. Just enough learning (of association rules): the tar2 "treatment" learner. Artif. Intell. Rev., 25(3):211--229, 2006.

Digital Library

[18]

C. Păsăreanu and N. Rungta. Symbolic PathFinder: symbolic execution of Java bytecode. In ASE, pages 179--180. ACM, 2010.

Digital Library

[19]

C. S. Păsăreanu, P. C. Mehlitz, D. H. 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. ISSTA, 2008.

Digital Library

[20]

C. S. Păsăreanu, J. Schumann, P. Mehlitz, M. Lowry, G. Karsai, H. Nine, and S. Neema. Model based analysis and test generation for flight software. In Proceedings of the Third IEEE International Conference on Space Mission Challenges for Information Technology, pages 83--90, Washington, DC, USA, 2009. IEEE Computer Society.

Digital Library

[21]

R. Santelices and M. J. Harrold. Exploiting program dependencies for scalable multiple-path symbolic execution. In ISSTA, pages 195--206, 2010.

Digital Library

[22]

K. Sen and G. Agha. A race-detection and flipping algorithm for automated testing of multi-threaded programs. In Proc. HVC, volume 4383 of LNCS, pages 166--182. Springer, 2007.

Digital Library

[23]

K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In Proc. ESEC/FSE-13, pages 263--272, New York, NY, USA, 2005. ACM.

Digital Library

[24]

S. Siegel, A. Mironova, G. Avrunin, and L. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In ISSTA, pages 157--168. ACM, 2006.

Digital Library

[25]

M. Souza, M. Borges, M. d'Amorim, and C. S. Păsăreanu. CORAL: solving complex constraints for Symbolic Pathfinder. Proc. NFM, 2011.

Digital Library

[26]

N. Tillmann and J. De Halleux. Pex: white box test generation for. NET. In TAP, pages 134--153. Springer-Verlag, 2008.

Digital Library

[27]

A. Tomb, G. Brat, and W. Visser. Variably interprocedural program analysis for runtime error detection. In Proc. ISSTA, pages 97--107, New York, NY, USA, 2007. ACM Press.

Digital Library

[28]

W. Visser, C. Păsăreanu, and R. Pelánek. Test input generation for Java containers using state matching. In ISSTA, pages 37--48. ACM New York, NY, USA, 2006.

Digital Library

[29]

T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. TACAS, pages 365--381, 2005.

Digital Library

Cited By

Jia FHan RHuang PLiu MMa FZhang JJust RFraser G(2023)Improving Bit-Blasting for Nonlinear Integer ConstraintsProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598034(14-25)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598034
Muduli SRoy S(2022)Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzingProceedings of the ACM on Programming Languages10.1145/35633326:OOPSLA2(1236-1263)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563332
Zhang GChen ZShuai ZZhang YWang J(2022)Synergizing Symbolic Execution and Fuzzing By Function-level Selective Symbolization2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00045(328-337)Online publication date: Dec-2022
https://doi.org/10.1109/APSEC57359.2022.00045
Show More Cited By

Index Terms

Symbolic execution with mixed concrete-symbolic solving

Recommendations

A Survey of Symbolic Execution Techniques

Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any ...
Symbolic execution and program testing

This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program (e.g. numbers) one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be ...
DART: directed automated random testing
PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation

We present a new tool, named DART, for automatically testing software that combines three main techniques: (1) automated extraction of the interface of a program with its external environment using static source-code parsing; (2) automatic generation of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA '11: Proceedings of the 2011 International Symposium on Software Testing and Analysis

July 2011

394 pages

ISBN:9781450305624

DOI:10.1145/2001420

General Chair:
Matthew Dwyer
University of Nebraska
,
Program Chair:
Frank Tip
IBM T.J. Watson Research Center

Copyright © 2011 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]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 July 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSTA '11

Sponsor:

SIGSOFT

ISSTA '11: International Symposium on Software Testing and Analysis

July 17 - 21, 2011

Ontario, Toronto, Canada

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

60
Total Citations
View Citations
906
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)4

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jia FHan RHuang PLiu MMa FZhang JJust RFraser G(2023)Improving Bit-Blasting for Nonlinear Integer ConstraintsProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598034(14-25)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598034
Muduli SRoy S(2022)Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzingProceedings of the ACM on Programming Languages10.1145/35633326:OOPSLA2(1236-1263)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563332
Zhang GChen ZShuai ZZhang YWang J(2022)Synergizing Symbolic Execution and Fuzzing By Function-level Selective Symbolization2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00045(328-337)Online publication date: Dec-2022
https://doi.org/10.1109/APSEC57359.2022.00045
Liu MShuai ZLiu LMa KMa K(2022)Optimal Refinement-based Array Constraint Solving for Symbolic Execution2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00042(299-308)Online publication date: Dec-2022
https://doi.org/10.1109/APSEC57359.2022.00042
Sun CLiu BFu ALiu YLiu H(2022)Path-directed source test case generation and prioritization in metamorphic testingJournal of Systems and Software10.1016/j.jss.2021.111091183(111091)Online publication date: Jan-2022
https://doi.org/10.1016/j.jss.2021.111091
Xu DLiu BFeng WMing JZheng QLi JYu QFreund SYahav E(2021)Boosting SMT solver performance on mixed-bitwise-arithmetic expressionsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454068(651-664)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454068
Li PMeng WLu KLuo C(2021)On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic ExecutionProceedings of the Web Conference 202110.1145/3442381.3450002(58-69)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3442381.3450002
Wang SShrestha NSubburaman AWang JWei MNagappan N(2021)Automatic Unit Test Generation for Machine Learning LibrariesProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00138(1548-1560)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00138
Pandey AKotcharlakota PRoy SZhang DMøller A(2019)Deferred concretization in symbolic execution via fuzzingProceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3293882.3330554(228-238)Online publication date: 10-Jul-2019
https://dl.acm.org/doi/10.1145/3293882.3330554
Chen FGunawan ALo DKim S(2019)InSPeCT: Iterated Local Search for Solving Path Conditions2019 IEEE 15th International Conference on Automation Science and Engineering (CASE)10.1109/COASE.2019.8843039(1724-1729)Online publication date: Aug-2019
https://doi.org/10.1109/COASE.2019.8843039
Show More Cited By

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents