Abstract
Dynamic Symbolic Execution (DSE) is an important method for testing of programs. An important system on DSE is KLEEĀ [1] which inputs a C/C++ program annotated with symbolic variables, compiles it into LLVM, and then emulates the execution paths of LLVM using a specified backtracking strategy. The major challenge in symbolic execution is path explosion. The method of abstraction learning [7] has been used to address this. The key step here is the computation of an interpolant to represent the learned abstraction.
TracerX, our tool, is built on top of KLEE and it implements and utilizes abstraction learning. The core feature in abstraction learning is subsumption of paths whose traversals are deemed to no longer be necessary due to similarity with already-traversed paths. Despite the overhead of computing interpolants, the pruning of the symbolic execution tree that interpolants provide often brings significant overall benefits. In particular, TracerX can fully explore many programs that would be impossible for any non-pruning system like KLEE to do so.
Chapter PDF
Similar content being viewed by others
References
Cadar, C., Dunbar, D., Engler, D.R., etĀ al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th OSDI. pp. 209ā224 (2008)
Chu, D.H., Jaffar, J.: A complete method for symmetry reduction in safety verification. In: 24th International Conference on Computer Aided Verification (CAV). pp. 616ā633, USA. Springer (2012)
Chu, D.H., Jaffar, J., Maghareh, R.: Precise cache timing analysis via symbolic execution. In: 22nd IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS). pp. 1ā12 (2016)
Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation (PLDI). pp. 213ā223 (2005)
Jaffar, J., Murali, V., Navas, J.A.: Boosting concolic testing via interpolation. In: Proceedings of the 9th Conference on Foundations of Software Engineering (FSE). pp. 48ā58 (2013)
Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: 24th International Conference on Computer Aided Verification (CAV). pp. 758ā766. Springer (2012)
Jaffar, J., Santosa, A.E., Voicu, R.: An interpolation method for CLP traversal. In: 15th International Conference on Principles and Practice of Constraint Programming (CP). pp. 454ā469. Springer (2009)
McMillan, K.L.: Lazy annotation for program testing and verification. In: 22ndInternational Conference on Computer Aided Verification (CAV). pp. 104ā118 (2010)
Mcmillan, K.L.: Lazy annotation revisited. In: 26th International Conference on Computer Aided Verification (CAV). pp. 243ā259 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
Ā© 2020 The Author(s)
About this paper
Cite this paper
Jaffar, J., Maghareh, R., Godboley, S., Ha, XL. (2020). TracerX: Dynamic Symbolic Execution with Interpolation (Competition Contribution). In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_28
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)