Abstract
This paper presents a novel technique for handling a precondition in dynamic symbolic execution (DSE) testing tools. It delays precondition constraints until the end of the program path evaluation. This method allows PathCrawler, a DSE tool for C programs, to accept a precondition defined as a C function. It provides a convenient way to express a precondition even for developers who are not familiar with specification formalisms. Our initial experiments show that it is more efficient than early precondition treatment, and has a limited overhead compared to a native treatment of a precondition directly expressed in constraints. It has also proven useful for combinations of static and dynamic analysis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Botella, B., Delahaye, M., Hong-Tuan-Ha, S., Kosmatov, N., Mouy, P., Roger, M., Williams, N.: Automating structural testing of C programs: Experience with PathCrawler. In: AST 2009 (2009)
Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: A tool for generating structurally complex test inputs. In: ICSE 2007 (2007)
Visser, W., Pǎsǎreanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: ISSTA 2004 (2004)
Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC/ FSE 2013 (2013)
Barnett, M., Fahndrich, M., de Halleux, P., Logozzo, F., Tillmann, N.: Exploiting the synergy between automated-test-generation and programming-by-contract. In: ICSE 2009 (2009)
Godefroid, P.: Compositional dynamic test generation. In: POPL 2007 (2007)
Kosmatov, N.: All-paths test generation for programs with internal aliases. In: ISSRE 2008 (2008)
Kosmatov, N.: Online version of PathCrawler (2010–2013), http://pathcrawler-online.com/
Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC 2012 (2012)
Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: SAC 2013 (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delahaye, M., Kosmatov, N. (2013). A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools. In: Legay, A., Bensalem, S. (eds) Runtime Verification. RV 2013. Lecture Notes in Computer Science, vol 8174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40787-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-40787-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40786-4
Online ISBN: 978-3-642-40787-1
eBook Packages: Computer ScienceComputer Science (R0)