nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Certifying Safety and Termination Proofs for Integer Transition Systems

verfasst von : Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada

Erschienen in: Automated Deduction – CADE 26

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms

Nächstes Kapitel Biabduction (and Related Problems) in Array Separation Logic

In the Isabelle formalization and the certificate XML, formulas are represented in negation normal form and conjunction and disjunction are not necessarily binary.

In the Isabelle formalization we admit auxiliary variables to appear in the transition formula. To ease readability we omit this ability in the paper.

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

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)CrossRef

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)MathSciNetCrossRefMATH

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

10.

Caleiro, C., Gonçalves, R.: On the algebraization of many-sorted logics. In: WADT 2006, pp. 21–36

11.

Cho, S., Kang, J., Choi, J., Yi, K.: SparrowBerry: a verified validator for an industrial-strength static analyzer. http://ropas.snu.ac.kr/sparrowberry/

12.

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

13.

Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS 2013, pp. 47–61

14.

Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006, pp. 415–426

15.

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)

16.

Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: RTA 2011, pp. 41–50

17.

Farkas, J.: Theorie der einfachen Ungleichungen. J. für die reine Angew. Math. 124, 1–27 (1902)MathSciNetMATH

18.

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)MathSciNetCrossRefMATH

19.

Heule, M.J., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD 2013, pp. 181–188. IEEE

20.

Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL 2015, pp. 247–259

21.

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)CrossRef

22.

Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: CAV 2014, pp. 17–34

23.

Lammich, P.: Verified efficient implementation of Gabow’s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014, pp. 325–340

24.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

25.

Marić, F., Janičić, P.: Formal correctness proof for DPLL procedure. Informatica 21(1), 57–78 (2010)MathSciNetMATH

26.

McMillan, K.: Lazy abstraction with interpolants. In: CAV 2006, pp. 123–136

27.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH

28.

Nipkow, T.: Linear quantifier elimination. J. Autom. Reason. 45(2), 189–212 (2010)MathSciNetCrossRefMATH

29.

Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: RTA 2010, pp. 259–276

30.

Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Hoboken (1999)MATH

31.

Spasić, M., Marić, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012, pp. 434–449

32.

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)CrossRef

33.

Sternagel, C., Thiemann, R.: The certification problem format. In: UITP 2014, EPTCS, vol. 167, pp. 61–72 (2014)

34.

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)MathSciNetCrossRefMATH

35.

Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: TPHOLs 2009, pp. 452–468

36.

Tseitin, G.S.: On the complexity of proof in prepositional calculus. Stud. Constr. Math. Math. Logic Part II 8, 234–259 (1968)MathSciNet

37.

Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: TACAS 2016, pp. 54–70

38.

Wang, H.: Logic of many-sorted theories. J. Symb. Logic 17(2), 105–116 (1952)MathSciNetCrossRefMATH

39.

Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL 2012, pp. 427–440

Titel: Certifying Safety and Termination Proofs for Integer Transition Systems
verfasst von: Marc Brockschmidt
Sebastiaan J. C. Joosten
René Thiemann
Akihisa Yamada
Verlag: Springer International Publishing
Buch: Automated Deduction – CADE 26
Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-63046-5_28

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"