Abstract
TRACER [8] is a tool for verifying safety properties of sequential C programs. TRACER attempts at building a finite symbolic execution graph which over-approximates the set of all concrete reachable states and the set of feasible paths.
We present an abstract framework for TRACER and similar CEGAR-like systems [2, 3, 5, 6, 9]. The framework provides (1) a graph-transformation based method for reducing the feasible paths in control-flow graphs, (2) a model for symbolic execution, subsumption, predicate abstraction and invariant generation. In this framework we formally prove two key properties: correct construction of the symbolic states and preservation of feasible paths. The framework focuses on core operations, leaving to concrete prototypes to “fit in” heuristics for combining them.
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
Notes
- 1.
Given an arbitrary configuration, there is no guarantee that there exists a fresh symbolic variable for a given program variable, since expressions are defined as total functions.
- 2.
This is ensured by a number of constraints on the free variable rb forcing the root of the red part to be the initial location of the black part, etc.
- 3.
The conjunction of 2 and 3 is equivalent to say that the source of \( ra \) is a pending point in the analysis.
- 4.
Note that in the second assumption of gt_calc_se_rel, unlike in Sect. 4.1, subpath has a fifth parameter: the subsumption relation of \( rb \).
References
Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reasoning 52(2), 123–153 (2014)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. STTT 9(5–6), 505–525 (2007)
Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Proceedings of TACAS 2005, pp. 570–574 (2005)
Denise, A., Gaudel, M.-C., Gouraud, S.-D., Lassaigne, R., Oudinet, J., Peyronnet, S.: Coverage-biased random exploration of large models and application to testing. Int. J. Softw. Tools Technol. Transfer 14(1), 73–93 (2011). ISSN 1433–2787
Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of PLDI 2012, pp. 405–416 (2012)
Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005)
Jaffar, J., Navas, J.A., Santosa, A.E.: Unbounded symbolic execution for program verification. In: Proceedings of RV 2011 (2011)
Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758–766. Springer, Heidelberg (2012)
McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL–A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Noschinski, L.: A Graph Library for Isabelle. Math. Comput. Sci. 9(1), 23–39 (2015). doi:10.1007/s11786-014-0183-z. ISSN 1661–8289. http://dx.doi.org/10.1007/s11786-014-0183-z
Acknowledgement
We thank Marie-Claude Gaudel for her support while doing this work and for her remarks on this article.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Aissat, R., Voisin, F., Wolff, B. (2016). Infeasible Paths Elimination by Symbolic Execution Techniques. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-43144-4_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-43143-7
Online ISBN: 978-3-319-43144-4
eBook Packages: Computer ScienceComputer Science (R0)