Cited By
View all- Laneve C(2024)Reachability Analysis in Micro-StipulaProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678247(1-12)Online publication date: 9-Sep-2024
Leveraging abstract interpretation for efficient dynamic symbolic execution
Abstract
Dynamic Symbolic Execution (DSE) is a technique to automatically generate test inputs by executing a program with concrete and symbolic values simultaneously. A key challenge in DSE is scalability; executing all feasible program paths is not possible, owing to the potentially exponential or infinite number of paths. Loops are a main source of path explosion, in particular where the number of iterations depends on a program's input. Problems arise because DSE maintains symbolic values that capture only the dependencies on symbolic inputs. This ignores control dependencies, including loop dependencies that depend indirectly on the inputs. We propose a method to increase the coverage achieved by DSE in the presence of input-data dependent loops and loop dependent branches. We combine DSE with abstract interpretation to find indirect control dependencies, including loop and branch indirect dependencies. Preliminary results show that this results in better coverage, within considerably less time compared to standard DSE.
References
[1]
N. Bjørner and A. Gurfinkel. Property directed polyhedral abstraction. In D. D’Souza et al., editor, Verification, Model Checking, and Abstract Interpretation (VMCAI’15), volume 8931 of Lecture Notes in Computer Science, pages 263–281. Springer, 2015.
[2]
P. ˇ Cadek, J. Strejˇcek, and M. Trt´ık. Tighter loop bound analysis. In Automated Technology for Verification and Analysis (ATVA’16), pages 512–527. Springer, 2016.
[3]
M. Christakis, P. Müller, and V. Wüstholz. Guiding dynamic symbolic execution toward unverified program executions. In Proc. 38th Int. Conf. Software Engineering (ICSE’16), pages 144–155. ACM, 2016.
[4]
P. Cousot. Abstract interpretation. ACM Computing Surveys, 28(2):324– 328, 1996.
[5]
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM Symp. Principles of Programming Languages (POPL’77), pages 238–252. ACM, 1977.
[6]
P. Cousot and N. Halbwachs. Automatic discovery of linear constraints among variables of a program. In Proc. Fifth ACM Symp. Principles of Programming Languages (POPL’78), pages 84–97. ACM, 1978.
[7]
CVE—common vulnerabilities and exposures, May 2017. http://cve. mitre.org/.
[8]
P. Dinges and G. Agha. Targeted test input generation using symbolicconcrete backward execution. In Proc. 29th ACM/IEEE Int. Conf. Automated Software Engineering (ASE’14), pages 31–36. ACM, 2014.
[9]
P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI’05), pages 213–223. ACM, 2005.
[10]
P. Godefroid and D. Luchaup. Automatic partial loop summarization in dynamic test generation. In Proc. 2011 Int. Symp. Software Testing and Analysis (ISSTA’11), pages 23–33. ACM, 2011.
[11]
B. Jeannet and A. Miné. Apron: A library of numerical abstract domains for static analysis. In A. Bouajjani and O. Maler, editors, Computer Aided Verification (CAV’09), volume 5643 of Lecture Notes in Computer Science, pages 661–667. Springer, 2009.
[12]
D. Kroening, N. Sharygina, S. Tonetta, A. Tsitovich, and C. M. Wintersteiger. Loop summarization using state and transition invariants. Formal Methods in System Design, 42(3):221–261, 2013.
[13]
F. Logozzo and M. Fähndrich. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In Proc. 2008 ACM Symp. Applied Computing, pages 184–188. ACM, 2008.
[14]
A. Miné. Weakly Relational Numerical Abstract Domains. PhD thesis, Ecole Polytechnique, 2004.
[15]
A. Miné. The Octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31–100, 2006.
[16]
P. Saxena, P. Poosankam, S. McCamant, and D. Song. Loop-extended symbolic execution on binary programs. In Proc. 18th Int. Symp. Software Testing and Analysis (ISSTA’09), pages 225–236. ACM, 2009.
[17]
K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In Proc. 10th European Software Engineering Conf., pages 263– 272. ACM, 2005.
[18]
N. Tillmann and J. De Halleux. Pex—white box test generation for .NET. In B. Beckert and R. Hähnle, editors, Tests and Proofs (TAP’08), volume 4966 of Lecture Notes in Computer Science, pages 134–153. Springer, 2008.
[19]
M. Trt´ık. Symbolic Execution and Program Loops. PhD thesis, Faculty of Informatics, Masaryk University, 2013.
[20]
A. J. Venet. The Gauge domain: Scalable analysis of linear inequality invariants. In P. Madushan and S. A. Seshia, editors, Computer Aided Verification, volume 7358 of Lecture Notes in Computer Science, pages 139–154. Springer, 2012.
[21]
X. Xiao, S. Li, T. Xie, and N. Tillmann. Characteristic studies of loop problems for structural test generation via symbolic execution. In Proc. 28th IEEE/ACM Int. Conf. Automated Software Engineering (ASE’13), pages 246–256. IEEE Comp. Soc., 2013.
Recommendations
Exploiting program dependencies for scalable multiple-path symbolic execution
ISSTA '10: Proceedings of the 19th international symposium on Software testing and analysisThis paper presents a new technique, called Symbolic Program Decomposition (or SPD), for symbolic execution of multiple paths that is more scalable than existing techniques, which symbolically execute control-flow paths individually. SPD exploits ...
Augmented dynamic symbolic execution
ASE '12: Proceedings of the 27th IEEE/ACM International Conference on Automated Software EngineeringDynamic symbolic execution (DSE) can efficiently explore all simple paths through a program, reliably determining whether there are any program crashes or violations of assertions or code contracts. However, if such automated oracles do not exist, the ...
MultiSE: multi-path symbolic execution using value summaries
ESEC/FSE 2015: Proceedings of the 2015 10th Joint Meeting on Foundations of Software EngineeringDynamic symbolic execution (DSE) has been proposed to effectively generate test inputs for real-world programs. Unfortunately, DSE techniques do not scale well for large realistic programs, because often the number of feasible execution paths of a ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2017
1033 pages
ISBN:9781538626849
- General Chair:
- Grigore Rosu,
- Program Chairs:
- Massimiliano Di Penta,
- Tien N. Nguyen
Sponsors
Publisher
IEEE Press
Publication History
Published: 30 October 2017
Author Tags
Qualifiers
- Article
Acceptance Rates
Overall Acceptance Rate 82 of 337 submissions, 24%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 213Total Downloads
- Downloads (Last 12 months)22
- Downloads (Last 6 weeks)4
Reflects downloads up to 26 Nov 2024
Other Metrics
Citations
Cited By
View all- Laneve C(2024)Reachability Analysis in Micro-StipulaProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678247(1-12)Online publication date: 9-Sep-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in