nach oben

Formal Methods in System Design

Erschienen in:

01.08.2013

Ranking function synthesis for bit-vector relations

verfasst von: Byron Cook, Daniel Kroening, Philipp Rümmer, Christoph M. Wintersteiger

Erschienen in: Formal Methods in System Design | Ausgabe 1/2013

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Ranking function synthesis is a key component of modern termination provers for imperative programs. While it is well-known how to generate linear ranking functions for relations over (mathematical) integers or rationals, efficient synthesis of ranking functions for machine-level integers (bit-vectors) is an open problem. This is particularly relevant for the verification of low-level code. We propose several novel algorithms to generate ranking functions for relations over machine integers: a complete method based on a reduction to Presburger arithmetic, and a template-matching approach for predefined classes of ranking functions based on reduction to SAT- and QBF-solving. The utility of our algorithms is demonstrated on examples drawn from Windows device drivers.

Vorheriger Artikel Automatic verification of competitive stochastic systems

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

Alternatively, pairs \(( \mathit {state} _{i}, \mathit {state} '_{i})\) of variables with width \(\alpha ( \mathit {state} _{i})= \alpha ( \mathit {state} '_{i})=1\) can be used.

This deviates from the terminology in [29], where integrality is attributed to polyhedra, and not to systems of inequalities. We choose to speak of integral systems of inequalities for sake of brevity.

http://www.philipp.ruemmer.org/seneschal.shtml.

In [11], it was incorrectly stated that the constant term in (17) is “1” instead of “2”.

Version 6, now superseded by the Windows Driver Kit; see http://msdn.microsoft.com/en-us/windows/hardware/gg581061.

http://www.cprover.org/goto-cc/.

Following the hypothesis that loop termination seldom depends on complex variables that are possibly calculated by other loops, our slicing algorithm replaces all assignments that depend on five or more variables with non-deterministic values, and all loops other than the analysed one with program fragments that havoc the program state (non-deterministic assignments to all variables that might change during the execution of the loop).

http://www.philipp.ruemmer.org/seneschal.shtml.

http://www7.in.tum.de/~rybal/rankfinder/.

Alglave J, Kroening D, Nimal V, Tautschnig M (2013) Software verification for weak memory via program transformation. In: European symposium on programming (ESOP). Lecture notes in computer science, vol 7792. Springer, Berlin, pp 512–532

Babic D, Hu AJ, Rakamaric Z, Cook B (2007) Proving termination by divergence. In: SEFM. IEEE Press, New York, pp 93–102

Ball T, Kupferman O, Sagiv M (2007) Leaping loops in the presence of abstraction. In: CAV. Lecture notes in computer science, vol 4590. Springer, Berlin, pp 491–503

Benedetti M (2005) sKizzo: a suite to evaluate and certify QBFs. In: CADE. Lecture notes in computer science, vol 3632. Springer, Berlin, pp 369–376

Biere A (2005) Resolve and expand. In: SAT. Lecture notes in computer science, vol 3542. Springer, Berlin, pp 59–70

Biere A, Artho C, Schuppan V (2002) Liveness checking as safety checking. In: FMICS. Electronic notes in theoretical computer science, vol 66. Elsevier, Amsterdam, pp 160–177

Bradley AR, Manna Z, Sipma HB (2005) Termination analysis of integer linear loops. In: CONCUR. Lecture notes in computer science, vol 3653. Springer, Berlin, pp 488–502

Brinkmann R, Drechsler R (2002) RTL-datapath verification using integer linear programming. In: Proc of VLSI design. IEEE Press, New York, pp 741–746

Clarke EM, Kroening D, Sharygina N, Yorav K (2004) Predicate abstraction of ANSI-C programs using SAT. Form Methods Syst Des 25(2–3):105–127 MATHCrossRef

10.

Colón M, Sipma H (2001) Synthesis of linear ranking functions. In: TACAS. Lecture notes in computer science, vol 2031. Springer, Berlin, pp 67–81

11.

Cook B, Kroening D, Rümmer P, Wintersteiger CM (2010) Ranking function synthesis for bit-vector relations. In: TACAS. Lecture notes in computer science, vol 6015. Springer, Berlin, pp 236–250

12.

Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: SAS. Lecture notes in computer science, vol 3672. Springer, Berlin, pp 87–101

13.

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

14.

Dams D, Gerth R, Grumberg O (2000) A heuristic for the automatic generation of ranking functions. In: Workshop on advances in verification, pp 1–8

15.

Encrenaz E, Finkel A (2009) Automatic verification of counter systems with ranking functions. In: INFINITY. Electronic notes in theoretical computer science, vol 239. Elsevier, Amsterdam, pp 85–103

16.

Falke S, Kapur D, Sinz C (2012) Termination analysis of imperative programs using bitvector arithmetic. In: VSTTE. Lecture notes in computer science, vol 7152. Springer, Berlin, pp 261–277

17.

Giunchiglia E, Narizzano M, Tacchella A (2004) QuBE++: an efficient QBF solver. In: FMCAD. Lecture notes in computer science, vol 3312. Springer, Berlin, pp 201–213

18.

Griggio A (2011) Effective word-level interpolation for software verification. In: Formal methods in computer-aided design (FMCAD). IEEE Press, New York, pp 28–36

19.

Horwitz S, Reps TW, Binkley D (1988) Interprocedural slicing using dependence graphs. In: PLDI. ACM, New York, pp 35–46

20.

Jussila T, Biere A (2007) Compressing BMC encodings with QBF. In: Workshop on bounded model checking (BMC’06). Electronic notes in theoretical computer science, vol 174. Elsevier, Amsterdam, pp 45–56

21.

Jussila T, Biere A, Sinz C, Kroening D, Wintersteiger CM (2007) A first step towards a unified proof checker for QBF. In: SAT. Lecture notes in computer science, vol 4501. Springer, Berlin, pp 201–214

22.

Kovásznai G, Fröhlich A, Biere A (2012) On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: SMT workshop at IJCAR

23.

Parthasarathy G, Iyer MK, Cheng KT, Wang LC (2004) An efficient finite-domain constraint solver for circuits. In: Design automation conference (DAC). ACM, New York, pp 212–217

24.

Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: VMCAI. Lecture notes in computer science, vol 2937. Springer, Berlin, pp 239–251

25.

Podelski A, Rybalchenko A (2004) Transition invariants. In: LICS. IEEE Press, New York, pp 32–41

26.

Podelski A, Rybalchenko A (2007) ARMC: The logical choice for software model checking with abstraction refinement. In: PADL. Lecture notes in computer science, vol 4354. Springer, Berlin, pp 245–259

27.

Presburger M (1930) Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Sprawozdanie z I kongresu metematyków slowiańskich, Warsaw, 1929, pp 92–101.

28.

Rümmer P (2008) A constraint sequent calculus for first-order logic with linear integer arithmetic. In: LPAR. Lecture notes in computer science, vol 5330. Springer, Berlin, pp 274–289

29.

Schrijver A (1986) Theory of linear and integer programming. Wiley, New York MATH

30.

Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time (preliminary report). In: STOC. ACM, New York, pp 1–9

31.

Wegner P (1960) A technique for counting ones in a binary computer. Commun ACM 3(5):322 CrossRef

32.

Wintersteiger CM, Hamadi Y, de Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42:3–23 CrossRef

33.

Yang H, Lee O, Berdine J, Calcagno C, Cook B, Distefano D, O’Hearn PW (2008) Scalable shape analysis for systems code. In: CAV. Lecture notes in computer science, vol 5123. Springer, Berlin, pp 385–398

Titel: Ranking function synthesis for bit-vector relations
verfasst von: Byron Cook
Daniel Kroening
Philipp Rümmer
Christoph M. Wintersteiger
Publikationsdatum: 01.08.2013
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 1/2013
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-013-0186-4

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

Springer Professional "Technik"