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
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 3/2018

31.08.2017

Automating regression verification of pointer programs by predicate abstraction

verfasst von: Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich

Erschienen in: Formal Methods in System Design | Ausgabe 3/2018

Einloggen

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

search-config
loading …

Abstract

Regression verification is an approach complementing regression testing with formal verification. The goal is to formally prove that two versions of a program behave either equally or differently in a precisely specified way. In this paper, we present a novel automated approach for regression verification that reduces the equivalence of two related imperative pointer programs to constrained Horn clauses over uninterpreted predicates. Subsequently, state-of-the-art SMT solvers are used to solve the clauses. We have implemented the approach, and our experiments show that non-trivial programs with integer and pointer arithmetic can now be proved equivalent without further user input.
Vorheriger Artikel Special issue: program equivalence
Nächster Artikel Automated verification of automata communicating via FIFO and bag buffers

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
A coupling predicate is an inductive two-program invariant that relates the two programs throughout their execution. We are typically interested in coupling predicates that imply result equality upon termination of both programs.
 
2
Our approach requires that the two programs which we prove equivalent have disjoint variable and function names. To distinguish equally named identifiers from the two programs, we add subscripts indicating the program to which they belong. We may also concurrently use the original identifiers without a subscript as long as the relation is clear from the context.
 
3
Our parser currently does not support preincrement expressions, so we rewrite the relevant code fragment as https://static-content.springer.com/image/art%3A10.1007%2Fs10703-017-0293-8/MediaObjects/10703_2017_293_Figr_HTML.gif when verifying with our tool.
 
4
Sometimes, it is desirable to model the behavior of a subroutine using nondeterminism (e.g., for library functions or memory allocation). This can be done in our approach by providing according specifications for the subroutines.
 
5
To simplify presentation, we will use the terms “statement list” and “program” interchangeably. The exact relation will be clear from the context.
 
6
Due to reasons of computability, sets of Horn clauses exist for which neither (i) nor (ii) can be returned: those are clauses that are solvable in a set-theoretic sense, but no solution can be expressed in the decidable language used for predicates. In such cases, usually non-termination occurs.
 
8
There are several reasons for the timings being different to those we previously reported in [17]. These include: different hardware, newer versions of all tools, and in particular Eldarica now used in client-server mode, which avoids JVM startup and warmup costs.
 
9
Loop unrolling is a simple transformation, in which the loop body is replicated within the loop and guarded by the loop guard. This transformation preserves the semantics of the program.
 
10
For the ease of presentation, we left out the unmodified variables \(a_1, n_1, a_2, n_2\) although they would appear in the predicate.
 
11
As explained in the introduction, in practice, one would not be checking the equivalence of a large system all at once, though.
 
Literatur
1.
2.
Almeida J, Barbosa M, Sousa Pinto J, Vieira B (2009) Verifying cryptographic software correctness with respect to reference implementations. In: Alpuente M, Cook B, Joubert C (eds) Formal methods for industrial critical systems. Lecture notes in computer science, vol 5825. Springer, Berlin, pp 37–52
3.
Ammann P, Offutt J (2008) Introduction to software testing, 1st edn. Cambridge University Press, New YorkCrossRef
4.
Amtoft T, Bandhakavi S, Banerjee A (2006) A logic for information flow in object-oriented programs. In: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL’06, pp 91–102. ACM, New York, NY, USA
5.
Backes J, Person S, Rungta N, Tkachuk O (2013) Regression verification using impact summaries. In: Bartocci E, Ramakrishnan C (eds) Model checking software. Lecture notes in computer science, vol 7976. Springer, Berlin, pp 99–116
6.
Banerjee A, Naumann DA (2005) Ownership confinement ensures representation independence for object-oriented programs. J ACM 52(6):894–960MathSciNetCrossRefMATH
7.
Banerjee A, Naumann DA (2005) State based ownership, reentrance, and encapsulation. In: Proceedings of the 19th European conference on object-oriented programming, ECOOP’05. Springer, Berlin, pp 387–411
8.
Barthe G, Crespo J, Grégoire B, Kunz C, Zanella Béguelin S (2012) Computer-aided cryptographic proofs. In: Beringer L, Felty A (eds) Interactive theorem proving. Lecture notes in computer science, vol 7406. Springer, Berlin, pp 11–27
9.
Barthe G, Crespo JM, Kunz C (2011) Relational verification using product programs. In: Butler M, Schulte W (eds) Proceedings of the 17th international symposium on formal methods (FM). Lecture notes in computer science, vol 6664. Springer, Berlin, pp 200–214
10.
Barthe G, D’Argenio PR, Rezk T (2004) Secure information flow by self-composition. In: 17th IEEE computer security foundations workshop, CSFW-17, Pacific Grove, CA, USA. IEEE Computer Society, pp 100–114
11.
Beckert B, Bruns D, Klebanov V, Scheben C, Schmitt PH, Ulbrich M (2013) Information flow in object-oriented software. In: Gupta G, Peña R (eds) 23rd international symposium on logic-based program synthesis and transformation (LOPSTR 2013). Dpto. de Systemas Informáticos y Computation, Universidad Complutense de Madrid, TR-11-13, pp 15–32
12.
Bjørner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified horn clauses. In: Logozzo F, Fähndrich M (eds) Proceedings of the 20th international symposium on static analysis, SAS 2013, Seattle, WA, USA, June 20–22, 2013. Lecture notes in computer science, vol 7935. Springer, pp 105–125. doi:10.​1007/​978-3-642-38856-9_​8
13.
Darvas A, Hähnle R, Sands D (2005) A theorem proving approach to analysis of secure information flow. In: Proceedings of the second international conference on security in pervasive computing, SPC’05. Springer, Berlin, pp 193–209
14.
15.
16.
Falke S, Kapur D, Sinz C (2012) Termination analysis of imperative programs using bitvector arithmetic. In: Proceedings of the 4th international conference on verified software: theories, tools, experiments (VSTTE’12). Springer, Berlin, pp 261–277
17.
Felsing D, Grebing S, Klebanov V, Rümmer P, Ulbrich M (2014) Automating regression verification. In: Proceedings of the 29th ACM/IEEE international conference on automated software engineering, ASE’14. ACM, pp 349–360
18.
Giesl J, Thiemann R, Schneider-Kamp P, Falke S (2004) Automated termination proofs with AProVE. In: van Oostrom V (ed) Proceedings of the 15th international conference on rewriting techniques and applications (RTA 2004). Lecture notes in computer science, vol 3091. Springer, pp 210–220
19.
Godlin B, Strichman O (2008) Inference rules for proving the equivalence of recursive procedures. Acta Inform 45(6):403–439MathSciNetCrossRefMATH
20.
Godlin B, Strichman O (2009) Regression verification. In: Proceedings of the 46th annual design automation conference, DAC’09. ACM, pp 466–471
21.
22.
Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: Proceedings of the 33rd ACM SIGPLAN conference on programming language design and implementation, PLDI’12. ACM, pp 405–416
23.
Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press, CambridgeCrossRefMATH
24.
25.
Hawblitzel C, Kawaguchi M, Lahiri SK, Rebêlo H (2013) Towards modularly comparing programs using automated theorem provers. In: Bonacina MP (ed) Proceedings of the 24th international conference on automated deduction, CADE-24, Lake Placid, NY, USA, June 9–14, 2013. Lecture notes in computer science, vol 7898, pp 282–299. Springer
26.
Hoder K, Bjørner N (2012) Generalized property directed reachability. In: Proceedings of the 15th international conference on theory and applications of satisfiability testing, SAT’12. Springer, Berlin, pp 157–171
27.
Huang SY, Cheng KT (1998) Formal equivalence checking and design debugging. Kluwer Academic Publishers, NorwellCrossRefMATH
28.
Lahiri SK, Hawblitzel C, Kawaguchi M, Rebêlo H (2012) SymDiff: a language-agnostic semantic diff tool for imperative programs. In: Proceedings of the 24th international conference on computer aided verification, CAV’12. Springer, Berlin, pp 712–717
29.
Lahiri SK, McMillan KL, Sharma R, Hawblitzel C (2013) Differential assertion checking. In: Proceedings of the 2013 9th joint meeting on foundations of software engineering, ESEC/FSE 2013. ACM, pp 345–355
30.
31.
McCarthy J (1962) Towards a mathematical science of computation. In: IFIP congress, pp 21–28
32.
Post H, Sinz C (2009) Proving functional equivalence of two AES implementations using bounded model checking. In: Proceedings of the 2009 international conference on software testing verification and validation, ICST’09. IEEE Computer Society, pp 31–40
33.
Rümmer P, Hojjat H, Kuncak V (2013) Disjunctive interpolants for Horn-clause verification. In: Proceedings of the 25th international conference on computer aided verification, CAV’13. Springer, Berlin, pp 347–363
34.
Scheben C, Schmitt PH (2014) Efficient self-composition for weakest precondition calculi. In: Jones CB, Pihlajasaari P, Sun J (eds) Proceedings, 19th international symposium on formal methods (FM). Lecture notes in computer science, vol 8442. Springer, pp 579–594
35.
van Eijk C (2000) Sequential equivalence checking based on structural similarities. IEEE Trans Comput Aided Des Integr Circuits Syst 19(7):814–819CrossRef
36.
37.
Verdoolaege S, Palkovic M, Bruynooghe M, Janssens G, Catthoor F (2010) Experience with widening based equivalence checking in realistic multimedia systems. J Electron Test 26(2):279–292CrossRef
38.
Welsch Y, Poetzsch-Heffter A (2012) Verifying backwards compatibility of object-oriented libraries using Boogie. In: Proceedings of the 14th workshop on formal techniques for Java-like programs, FTfJP’12. ACM, pp 35–41
39.
Wood T, Drossopoulou S, Lahiri SK, Eisenbach S (2017) Modular verification of procedure equivalence in the presence of memory allocation. In: Proceedings of the 26th European symposium on programming languages and systems, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, pp 937–963. doi:10.​1007/​978-3-662-54434-1_​35
Metadaten
Titel
Automating regression verification of pointer programs by predicate abstraction
verfasst von
Vladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
Publikationsdatum
31.08.2017
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 3/2018
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-017-0293-8

Premium Partner

    Bildnachweise