Abstract
Modern program analyzers translate imperative programs to an intermediate formal language like integer transition systems (ITSs), and then analyze properties of ITSs. Because of the high complexity of the task, a number of incorrect proofs are revealed annually in the Software Verification Competitions.
In this paper, we establish the trustworthiness of termination and safety proofs for ITSs. To this end we extend our Isabelle/HOL formalization IsaFoR by formalizing several verification techniques for ITSs, such as invariant checking, ranking functions, etc. Consequently the extracted certifier CeTA can now (in)validate safety and termination proofs for ITSs. We also adapted the program analyzers T2 and AProVE to produce machine-readable proof certificates, and as a result, most termination proofs generated by these tools on a standard benchmark set are now certified.
This work was partially supported by FWF project Y757. The authors are listed in alphabetical order regardless of individual contributions or seniority. We thank the anonymous reviewers for their helpful comments.
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.
In the Isabelle formalization and the certificate XML, formulas are represented in negation normal form and conjunction and disjunction are not necessarily binary.
- 2.
In the Isabelle formalization we admit auxiliary variables to appear in the transition formula. To ease readability we omit this ability in the paper.
- 3.
In the paper we use symbols \(\ge \) and > also for formulas. In the formalization we encode, e.g., by a formula \(e_1 \ge _\mathsf {f} e_2\) such that \(\alpha \models e_1 \ge _\mathsf {f} e_2\) iff \([\![e_1]\!]_\alpha \ge [\![e_2]\!]_\alpha \).
References
Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: FMOODS 2008, pp. 2–18
Albert, E., Bubel, R., Genaim, S., Hähnle, R., Puebla, G., Román-Díez, G.: A formal verification framework for static analysis. Softw. Syst. Model. 15(4), 987–1012 (2016)
Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: FSE 2016, pp. 326–337. ACM (2016)
Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 25–44. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_4
Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827–859 (2011)
Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: TACAS 2017 (to appear)
Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: ICALP 2005, pp. 1349–1361
Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: CAV 2013, pp. 413–429
Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: TACAS 2016, pp. 387–393
Caleiro, C., Gonçalves, R.: On the algebraization of many-sorted logics. In: WADT 2006, pp. 21–36
Cho, S., Kang, J., Choi, J., Yi, K.: SparrowBerry: a verified validator for an industrial-strength static analyzer. http://ropas.snu.ac.kr/sparrowberry/
Contejean, E., Paskevich, A., Urbain, X., Courtieu, P., Pons, O., Forest, J.: A3PAT, an approach for certified automated termination proofs. In: PEPM 2010, pp. 63–72
Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS 2013, pp. 47–61
Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006, pp. 415–426
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252 (1977)
Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: RTA 2011, pp. 41–50
Farkas, J.: Theorie der einfachen Ungleichungen. J. für die reine Angew. Math. 124, 1–27 (1902)
Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58, 3–31 (2017)
Heule, M.J., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD 2013, pp. 181–188. IEEE
Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL 2015, pp. 247–259
Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine and compiler. ACM Trans. Progr. Lang. Syst. 28(4), 619–695 (2006)
Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: CAV 2014, pp. 17–34
Lammich, P.: Verified efficient implementation of Gabow’s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014, pp. 325–340
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Marić, F., Janičić, P.: Formal correctness proof for DPLL procedure. Informatica 21(1), 57–78 (2010)
McMillan, K.: Lazy abstraction with interpolants. In: CAV 2006, pp. 123–136
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Nipkow, T.: Linear quantifier elimination. J. Autom. Reason. 45(2), 189–212 (2010)
Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: RTA 2010, pp. 259–276
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Hoboken (1999)
Spasić, M., Marić, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012, pp. 434–449
Spoto, F., Mesnard, F., Payet, É.: A termination analyser for Java Bytecode based on path-length. ACM Trans. Progr. Lang. Syst. 32(3), 8: 1–8: 70 (2010)
Sternagel, C., Thiemann, R.: The certification problem format. In: UITP 2014, EPTCS, vol. 167, pp. 61–72 (2014)
Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P., Aschermann, C.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason. 58, 33–65 (2017)
Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: TPHOLs 2009, pp. 452–468
Tseitin, G.S.: On the complexity of proof in prepositional calculus. Stud. Constr. Math. Math. Logic Part II 8, 234–259 (1968)
Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: TACAS 2016, pp. 54–70
Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105–116 (1952)
Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL 2012, pp. 427–440
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Brockschmidt, M., Joosten, S.J.C., Thiemann, R., Yamada, A. (2017). Certifying Safety and Termination Proofs for Integer Transition Systems. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-63046-5_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63045-8
Online ISBN: 978-3-319-63046-5
eBook Packages: Computer ScienceComputer Science (R0)