Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 1/2017

22.10.2016

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

verfasst von: Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp, Cornelius Aschermann

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2017

Einloggen

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

search-config
loading …

Abstract

While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic fully automatically was still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that over-approximates all possible runs of a program and that can be used to prove memory safety. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.
Vorheriger Artikel Analyzing Program Termination and Complexity Automatically with AProVE
Nächster Artikel The Bayesian Ontology Language

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 "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

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
Fußnoten
1
This LLVM program corresponds to the code obtained from strlen with the Clang compiler [23]. To ease readability, we wrote variables without “%” in front (i.e., we wrote “str” instead of “%str” as in proper LLVM) and added line numbers.
 
2
We use “\(\hookrightarrow \)” instead of “\(\mapsto \)” in separation logic, since \( mem \models n_1 \mapsto n_2\) would imply that \( mem (n)\) is undefined for all \(n \ne n_1\). This would be inconvenient in our formalization, since \( PT \) usually only contains information about a part of the allocated memory.
 
3
A corresponding representation could also be defined for big-endian layout. This layout information is necessary to decide which concrete states are represented by abstract states, but it is not used when constructing symbolic execution graphs (i.e., our remaining approach is independent of such layout information).
 
4
We identify sets of first-order formulas \(\{\varphi _1,\ldots , \varphi _n\}\) with their conjunction \(\varphi _1 \wedge \cdots \wedge \varphi _n\). Thus, \( CS \) is identified with the set resp. with the conjunction of the equations \(\bigcup _{1 \le i \le n} \{ \texttt {x}_i = LV _i(\texttt {x}) \mid \texttt {x} \in \mathcal {V}_{\mathcal {P}}, LV _i(\texttt {x}) \text { is defined}\}\). Moreover, we wrote https://static-content.springer.com/image/art%3A10.1007%2Fs10817-016-9389-x/MediaObjects/10817_2016_9389_IEq255_HTML.gif to ensure that this part of the formula is \( true \) if \( AL ^*= \varnothing \).
 
5
The reason is that then there is an address \( end \in {\mathbb {N}}_{>0}\) with \( end \ge as ^c(\texttt {str}_1)\) such that \( mem ^c( end ) = 0\) and \( mem ^c\) is defined for all numbers between \( as ^c(\texttt {str}_1)\) and \( end \). Hence if a is the state in (\(\dagger \)), then \( mem ^c \models \sigma (\langle {a}\rangle _{ SL })\) holds for any instantiation \(\sigma \) with \(\sigma (u_{\texttt {str}}) = as ^c(\texttt {str}_1)\), \(\sigma (v_{ end }) = end \), and \(\sigma (z) = 0\).
 
6
For any terms, “\(\llbracket {}t_1,\,t_2\rrbracket \; \bot \; \llbracket {}\overline{t_1},\,\overline{t_2}\rrbracket \)” is a shorthand for \(t_2< \overline{t_1} \vee \overline{t_2} < t_1\).
 
7
Analogous refinement rules can also be used for other conditional LLVM instructions, e.g., conditional jumps with br or other cases of icmp.
 
8
Since we do not consider struct data structures in this paper, we disregard getelementptr instructions with more than two parameters. Note that getelementptr instructions with just two parameters suffice for several levels of de-referencing (where memory has to be accessed after each getelementptr instruction).
 
9
Evaluation edges are edges that are not refinement or generalization edges.
 
10
This step corresponds to other work for machine-checked abstract interpreters [9, 17, 46].
 
11
For programs starting in states represented by an abstract state \(a_0\), it would suffice to prove termination of all \(\rightarrow _{{\mathcal {I}}}\)-evaluations starting in ITS states of the form \((a_0,\sigma )\).
 
12
In the transition, we do not impose the additional constraints of \(\langle {\overline{a}}\rangle \) on the post-variables \({\mathcal {V}}'\), since they are checked anyway in the next transition which starts in \(\overline{a}\).
 
13
The instructions supported by our implementation are icmp (eq,ne,sgt,sge,slt,sle, ugt,uge,ult,ule), add, sub, mul, sdiv, srem, urem, and, or, xor, shl, ashr, lshr, call, br, bitcast, ptrtoint, trunc, sext, zext, getelementptr (with at most 2 parameters), select, phi, ret, alloca, load, and store.
 
16
As mentioned above, we also started implementing support for non-termination in AProVE. When running the tools on all 631 C examples, AProVE proves termination for 409 and non-termination for 91 examples. Ultimate shows termination for 392 and non-termination for 111 programs. Finally, HipTNT+ proves termination in 312 and non-termination in 107 cases. Again, the detailed results can be found at [3].
 
Literatur
1.
Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Proceedings of CAV’12
2.
Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Proceedings of FMOODS’08
3.
4.
Berdine, J., Cook, B., Distefano, D., O’Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Proceedings of CAV’06
5.
Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O’Hearn, P.W.: Variance analyses from invariance analyses. In: Proceedings of POPL’07
6.
Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: Proceedings of CAV’11
7.
Bertot, Y., Castéran, P.: Coq Art. Springer, 2004
8.
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. 4, 827–859 (2011)MathSciNetCrossRefMATH
9.
Bodin, M., Jensen, T., Schmitt, A.: Certified abstract interpretation with pretty-big-step semantics. In: Proceedings of CPP’15
10.
Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. Formal Methods Syst. Design 38(2), 158–192 (2011)CrossRefMATH
11.
Brockschmidt, M., Otto, C., von Essen, C., Giesl, J.: Termination graphs for Java Bytecode. In: Verification, Induction, Termination Analysis, LNAI 6463, (2010)
12.
Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: Proceedings of RTA’11
13.
Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Proceedings of FoVeOOS’11
14.
Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Proceedings of CAV’12
15.
Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Proceedings of CAV’13
16.
Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: Proceedings of SAS’14
17.
Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Proceedings of ITP’10
18.
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of OSDI’08
19.
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In: Proceedings of SAS’06
20.
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Space invading systems code. In: Proceedings of LOPSTR’08
21.
Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of C programs. In: Proceedings of NFM’11
22.
Chen, H.Y., David, C., Kroening, D., Schrammel, P., Wächter, N.: Synthesising interprocedural bit-precise termination proofs. In: Proceedings of ASE’15
23.
24.
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRefMATH
25.
Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Proceedings of RTA’11
26.
Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Proceedings of SAS’05
27.
Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of PLDI’06
28.
Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: no return!. Formal Methods Syst. Design 35(3), 369–387 (2009)CrossRefMATH
29.
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL’78
30.
David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Proceedings of ESOP’15
31.
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS’08
32.
D’Silva, V., Urban, C.: Conflict-driven conditional termination. In: Proceedings of CAV’15
33.
Dudka, K., Peringer, P., Vojnar, T.: Predator: A shape analyzer based on symbolic memory graphs (competition contribution). In: Proceedings of TACAS’14
34.
35.
Falke, S., Kapur, D., Sinz. C.: Termination analysis of C programs using compiler intermediate languages. In: Proceedings of RTA’11
36.
Falke, S., Merz, F., Sinz, C.: LLBMC: Improved bounded model checking of C using LLVM (competition contribution). In: Proceedings of TACAS’13
37.
Fuhs, C., Giesl, J., Plücker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: Proceedings of RTA’09
38.
Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Proceedings of IJCAR’14
39.
Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. In: Proceedings of PLDI’15
40.
Gulwani, S., Tiwari, A.: An abstract domain for analyzing heap-manipulating low-level software. In: Proceedings of CAV’07
41.
Habermehl, P., Iosif, R., Rogalewicz, A., Vojnar, T.: Proving termination of tree manipulating programs. In: Proceedings of ATVA’07
42.
Harris, W.R., Lal, A., Nori, A., Rajamani, S.K.: Alternation for termination. In: Proceedings of SAS’10
43.
Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Proceedings of ATVA’13
44.
Hensel, J., Giesl, J., Frohn, F., Ströder, T.: Proving termination of programs with bitvector arithmetic by symbolic execution. In: Proceedings of SEFM’16
45.
Iosif, R., Rogalewicz, A.: Automata-based termination proofs. Comput. Inf. 32(4), 739–775 (2013)MathSciNetMATH
46.
Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Proceedings of POPL’15
47.
Kop, C., Nishida, N.: Automatic constrained rewriting induction towards verifying procedural programs. In: Proceedings of APLAS’14
48.
Kop, C., Nishida, N.: Constrained Term Rewriting tooL. In: Proceedings of LPAR’15
49.
Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C. M.: Termination analysis with compositional transition invariants. In: Proceedings of CAV’10
50.
Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio A.: Proving termination of imperative programs using Max-SMT. In: Proceedings of FMCAD’13
51.
Lattner, C., Adve V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of CGO’04
52.
Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: Proceedings of PLDI’15
53.
54.
Löwe, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: Proceedings of TACAS’14
55.
56.
Magill, S., Tsai, M., Lee, P., Tsay, Y.: Automatic numeric abstractions for heap-manipulating programs. In: Proceedings of POPL’10
57.
58.
Moy, Y., Marché, C.: Modular inference of subprogram contracts for safety checking. J. Symb. Comput., 45(11), 2010
59.
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM, 53(6), 2006
60.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002
61.
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of CSL’01
62.
63.
Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proceedings of RTA’10
64.
Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Proceedings of PADL’07
65.
Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL’95
66.
Spoto, F., Mesnard, F., Payet, É.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS, 32(3), 2010
67.
Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: Proceedings of IJCAR’14
68.
Ströder, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: Termination and memory safety of C programs (competition contribution). In: Proceedings of TACAS’15
69.
Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Proceedings of TPHOLs’09
70.
Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Proceedings of TACAS’11
71.
Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Proceedings of TACAS’16
72.
73.
Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM IR for verified program transformations. In: Proceedings of POPL’12
Metadaten
Titel
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
verfasst von
Thomas Ströder
Jürgen Giesl
Marc Brockschmidt
Florian Frohn
Carsten Fuhs
Jera Hensel
Peter Schneider-Kamp
Cornelius Aschermann
Publikationsdatum
22.10.2016
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9389-x

Weitere Artikel der Ausgabe 1/2017

Journal of Automated Reasoning 1/2017 Zur Ausgabe

OriginalPaper

The Bayesian Ontology Language

OriginalPaper

Soundness and Completeness Proofs by Coinductive Methods

OriginalPaper

An Approximation Framework for Solvers and Decision Procedures

OriginalPaper

Finding Proofs in Tarskian Geometry

EditorialNotes

Preface

OriginalPaper

Analyzing Program Termination and Complexity Automatically with AProVE

Premium Partner

    Bildnachweise