Skip to main content
Top
Published in: Formal Methods in System Design 1/2013

01-08-2013

Ranking function synthesis for bit-vector relations

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

Published in: Formal Methods in System Design | Issue 1/2013

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

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!

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!

Footnotes
1
Alternatively, pairs \(( \mathit {state} _{i}, \mathit {state} '_{i})\) of variables with width \(\alpha ( \mathit {state} _{i})= \alpha ( \mathit {state} '_{i})=1\) can be used.
 
2
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.
 
4
In [11], it was incorrectly stated that the constant term in (17) is “1” instead of “2”.
 
5
Version 6, now superseded by the Windows Driver Kit; see http://​msdn.​microsoft.​com/​en-us/​windows/​hardware/​gg581061.
 
7
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).
 
Literature
1.
go back to reference 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 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
2.
go back to reference Babic D, Hu AJ, Rakamaric Z, Cook B (2007) Proving termination by divergence. In: SEFM. IEEE Press, New York, pp 93–102 Babic D, Hu AJ, Rakamaric Z, Cook B (2007) Proving termination by divergence. In: SEFM. IEEE Press, New York, pp 93–102
3.
go back to reference 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 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
4.
go back to reference 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 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
5.
go back to reference Biere A (2005) Resolve and expand. In: SAT. Lecture notes in computer science, vol 3542. Springer, Berlin, pp 59–70 Biere A (2005) Resolve and expand. In: SAT. Lecture notes in computer science, vol 3542. Springer, Berlin, pp 59–70
6.
go back to reference 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 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
7.
go back to reference 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 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
8.
go back to reference Brinkmann R, Drechsler R (2002) RTL-datapath verification using integer linear programming. In: Proc of VLSI design. IEEE Press, New York, pp 741–746 Brinkmann R, Drechsler R (2002) RTL-datapath verification using integer linear programming. In: Proc of VLSI design. IEEE Press, New York, pp 741–746
9.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: PLDI. ACM, New York, pp 415–426 Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: PLDI. ACM, New York, pp 415–426
14.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference Horwitz S, Reps TW, Binkley D (1988) Interprocedural slicing using dependence graphs. In: PLDI. ACM, New York, pp 35–46 Horwitz S, Reps TW, Binkley D (1988) Interprocedural slicing using dependence graphs. In: PLDI. ACM, New York, pp 35–46
20.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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.
go back to reference Podelski A, Rybalchenko A (2004) Transition invariants. In: LICS. IEEE Press, New York, pp 32–41 Podelski A, Rybalchenko A (2004) Transition invariants. In: LICS. IEEE Press, New York, pp 32–41
26.
go back to reference 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 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.
go back to reference 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. 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.
go back to reference 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 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.
go back to reference Schrijver A (1986) Theory of linear and integer programming. Wiley, New York MATH Schrijver A (1986) Theory of linear and integer programming. Wiley, New York MATH
30.
go back to reference Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time (preliminary report). In: STOC. ACM, New York, pp 1–9 Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time (preliminary report). In: STOC. ACM, New York, pp 1–9
31.
go back to reference Wegner P (1960) A technique for counting ones in a binary computer. Commun ACM 3(5):322 CrossRef Wegner P (1960) A technique for counting ones in a binary computer. Commun ACM 3(5):322 CrossRef
32.
go back to reference Wintersteiger CM, Hamadi Y, de Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42:3–23 CrossRef Wintersteiger CM, Hamadi Y, de Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42:3–23 CrossRef
33.
go back to reference 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 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
Metadata
Title
Ranking function synthesis for bit-vector relations
Authors
Byron Cook
Daniel Kroening
Philipp Rümmer
Christoph M. Wintersteiger
Publication date
01-08-2013
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 1/2013
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-013-0186-4

Premium Partner