Abstract
Detection of infeasible code has recently been identified as a scalable and automated technique to locate likely defects in software programs. Given the (acyclic) control-flow graph of a procedure, infeasible code detection depends on an exhaustive search for feasible paths through the graph. A number of encodings of control-flow graphs into logic (understood by theorem provers) have been proposed in the past for this application. In this paper, we compare the performance of these different encodings in terms of runtime and the number of queries processed by the prover. We present a theory of acyclic control-flow as an alternative method of handling control-flow graphs. Such a theory can be built into theorem provers by means of theory plug-ins. Our experiments show that such native handling of control-flow can lead to significant performance gains, compared to previous encodings.
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.
Similar content being viewed by others
References
Arlt, S., Liu, Z., Schäf, M.: Reconstructing paths for reachable code. In: ICFEM (to appear, 2013)
Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. SIGSOFT SEN 31 (September 2005)
Bertolini, C., Schäf, M., Schweitzer, P.: Infeasible code detection. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 310–325. Springer, Heidelberg (2012)
Christ, J., Hoenicke, J., Schäf, M.: Towards bounded infeasible code detection. CoRR, abs/1205.6527 (2012)
Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS. LNCS, vol. 6887, pp. 351–368. Springer, Heidelberg (2011)
Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: a general approach to inferring errors in systems code. In: SOSP (2001)
Hoenicke, J., Leino, K.R., Podelski, A., Schäf, M., Wies, T.: Doomed program points. FMSD (2010)
Hovemeyer, D., Pugh, W.: Finding bugs is easy. In: OOPSLA (2004)
Johnson, D.S.: Approximation algorithms for combinatorial problems, vol. 9 (1974)
Leino, K.R.M., Rümmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312–327. Springer, Heidelberg (2010)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6) (2006)
Raz, R., Safra, S.: A sub-constant error-probability low-degree test, and a sub-constant error-probability PCP characterization of NP. In: STOC (1997)
Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008)
Tomb, A., Flanagan, C.: Detecting inconsistencies via universal reachability analysis. In: ISSTA
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Arlt, S., Rümmer, P., Schäf, M. (2013). A Theory for Control-Flow Graph Exploration. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_44
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_44
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)