Skip to main content
SpringerLink
Log in

Finding Inconsistencies in Programs with Loops

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9450))

Included in the following conference series:

Abstract

Inconsistent code is an important class of program abnormalities that appears in real-world code bases and often reveals serious bugs. A piece of code is inconsistent if it is not part of any safely terminating execution. Existing approaches to inconsistent code detection scale to programs with millions of lines of code, and have lead to patches in applications like the web-server Tomcat or the Linux kernel. However, the ability of existing tools to detect inconsistencies is limited by gross over-approximation of looping control-flow. We present a novel approach to inconsistent code detection that can reason about programs with loops without compromising precision. To that end, by leveraging recent advances in software model checking and Horn clause solving, we demonstrate how to encode the problem as a sequence of Horn clauses queries enabling us to detect inconsistencies that were previously unattainable.

This material is based upon work supported by the National Science Foundation under Grant No. 1422705, AFRL contract No. FA8750-15-C-0010, and NASA contract NNX14AI05A.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In presence of function calls, a CHC will have at least two predicate symbols in its body: one that represents the callee and the other modelling the successor. If callsites are ignored then CHCs will have only one predicate symbol modelling the successor.

  2. 2.

    For clarity, we have eliminated from the invariants all crumb variables.

  3. 3.

    https://github.com/seahorn/seahorn/tree/inconsistency/play/inconsistency.

References

  1. Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672–678. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  2. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25–32 (2009)

    Google Scholar 

  5. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Gurevich Festschrift II 2015. LNCS, vol. 9300, pp. 24–51. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  6. Blackshear, S., Lahiri, S.K.: Almost-correct specifications: a modular semantic framework for assigning confidence to warnings. In: PLDI, pp. 209–218 (2013)

    Google Scholar 

  7. Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 4–4. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  8. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: a tool for verifying programs through transformations. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 568–574. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  9. Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Dillig, I., Dillig, T., Aiken, A.: Static error detection using semantic inconsistency inference. In: PLDI, pp. 435–445 (2007)

    Google Scholar 

  11. 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)

    Google Scholar 

  12. Ermis, E., Schäf, M., Wies, T.: Error invariants. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187–201. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Flanagan, C.: Automatic software model checking via constraint logic. Sci. Comput. Program. 50(1–3), 253–270 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  14. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405–416 (2012)

    Google Scholar 

  15. Gurfinkel, A., Chaki, S., Sapra, S.: Efficient predicate abstraction of program summaries. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 131–145. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  17. Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  18. Hoenicke, J., Leino, K.R.M., Podelski, A., Schäf, M., Wies, T.: It’s doomed; we can prove it. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 338–353. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Hoenicke, J., Leino, K.R.M., Podelski, A., Schäf, M., Wies, T.: Doomed program points. In: FMSD, pp. 171–199 (2010)

    Google Scholar 

  20. Hovemeyer, D., Pugh, W.: Finding more null pointer bugs, but not too many. In: PASTE, pp. 9–14 (2007)

    Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS, pp. 23–30 (2007)

    Google Scholar 

  23. Jose, M., Majumdar, R.: Bug-assist: assisting fault localization in ANSI-C programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 504–509. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17–34. Springer, Heidelberg (2014)

    Google Scholar 

  25. Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846–862. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Lattner, C., Adve, V.S.: Automatic pool allocation: improving performance by controlling data structure layout in the heap. In: PLDI, pp. 129–142 (2005)

    Google Scholar 

  27. McCarthy, T., Rümmer, P., Schäf, M.: Bixie: finding and understanding inconsistent code. In: ICSE, pp. 645–648 (2015)

    Google Scholar 

  28. Peralta, J.C., Gallagher, J.P., Saglam, H.: Analysis of imperative programs through analysis of constraint logic programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 246–261. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  29. Popeea, C., Rybalchenko, A.: Threader: a verifier for multi-threaded programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 633–636. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  30. Rümmer, P., Hojjat, H., Kuncak, V.: Classifying and solving horn clauses for verification. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 1–21. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  31. Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347–363. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  32. Schäf, M., Schwartz-Narbonne, D., Wies, T.: Explaining inconsistent code. In: ESEC/FSE, pp. 521–531 (2013)

    Google Scholar 

  33. SeaHorn Inconsistency Checker. https://github.com/seahorn/seahorn/tree/inconsistency

  34. Tomb, A., Flanagan, C.: Detecting inconsistencies via universal reachability analysis. In: ISSTA, pp. 287–297 (2012)

    Google Scholar 

  35. Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: A differential approach to undefined behavior detection. TOCS 33(1), 1–29 (2015)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University, Pittsburgh, USA

    Temesghen Kahsai

  2. NASA Ames Research Center/SGT, Mountain View, USA

    Jorge A. Navas

  3. SRI International, Menlo Park, USA

    Dejan Jovanović & Martin Schäf

Authors
  1. Temesghen Kahsai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jorge A. Navas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Dejan Jovanović
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martin Schäf
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Schäf .

Editor information

Editors and Affiliations

  1. New York University, New York, New York, USA

    Martin Davis

  2. University of the South Pacific, Suva, Fiji

    Ansgar Fehnker

  3. Macquarie University, Sydney, New South Wales, Australia

    Annabelle McIver

  4. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kahsai, T., Navas, J.A., Jovanović, D., Schäf, M. (2015). Finding Inconsistencies in Programs with Loops. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48899-7_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48898-0

  • Online ISBN: 978-3-662-48899-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation