{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T05:46:46Z","timestamp":1757310406625},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,21]],"date-time":"2013-03-21T00:00:00Z","timestamp":1363824000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10703-013-0186-4","type":"journal-article","created":{"date-parts":[[2013,3,20]],"date-time":"2013-03-20T15:07:33Z","timestamp":1363792053000},"page":"93-120","source":"Crossref","is-referenced-by-count":16,"title":["Ranking function synthesis for bit-vector relations"],"prefix":"10.1007","volume":"43","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,3,21]]},"reference":[{"key":"186_CR1","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/978-3-642-37036-6_28","volume-title":"European symposium on programming (ESOP)","author":"J Alglave","year":"2013","unstructured":"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\u2013532"},{"key":"186_CR2","first-page":"93","volume-title":"SEFM","author":"D Babic","year":"2007","unstructured":"Babic D, Hu AJ, Rakamaric Z, Cook B (2007) Proving termination by divergence. In: SEFM. IEEE Press, New York, pp 93\u2013102"},{"key":"186_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-73368-3_50","volume-title":"CAV","author":"T Ball","year":"2007","unstructured":"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\u2013503"},{"key":"186_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"CADE","author":"M Benedetti","year":"2005","unstructured":"Benedetti M (2005) sKizzo: a\u00a0suite to evaluate and certify QBFs. In: CADE. Lecture notes in computer science, vol 3632. Springer, Berlin, pp 369\u2013376"},{"key":"186_CR5","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"SAT","author":"A Biere","year":"2005","unstructured":"Biere A (2005) Resolve and expand. In: SAT. Lecture notes in computer science, vol 3542. Springer, Berlin, pp 59\u201370"},{"key":"186_CR6","series-title":"Electronic notes in theoretical computer science","first-page":"160","volume-title":"FMICS","author":"A Biere","year":"2002","unstructured":"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\u2013177"},{"key":"186_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1007\/11539452_37","volume-title":"CONCUR","author":"AR Bradley","year":"2005","unstructured":"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\u2013502"},{"key":"186_CR8","first-page":"741","volume-title":"Proc of VLSI design","author":"R Brinkmann","year":"2002","unstructured":"Brinkmann R, Drechsler R (2002) RTL-datapath verification using integer linear programming. In: Proc of VLSI design. IEEE Press, New York, pp 741\u2013746"},{"issue":"2\u20133","key":"186_CR9","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"EM Clarke","year":"2004","unstructured":"Clarke EM, Kroening D, Sharygina N, Yorav K (2004) Predicate abstraction of ANSI-C programs using SAT. Form Methods Syst Des 25(2\u20133):105\u2013127","journal-title":"Form Methods Syst Des"},{"key":"186_CR10","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"TACAS","author":"M Col\u00f3n","year":"2001","unstructured":"Col\u00f3n M, Sipma H (2001) Synthesis of linear ranking functions. In: TACAS. Lecture notes in computer science, vol 2031. Springer, Berlin, pp 67\u201381"},{"key":"186_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/978-3-642-12002-2_19","volume-title":"TACAS","author":"B Cook","year":"2010","unstructured":"Cook B, Kroening D, R\u00fcmmer P, Wintersteiger CM (2010) Ranking function synthesis for bit-vector relations. In: TACAS. Lecture notes in computer science, vol 6015. Springer, Berlin, pp 236\u2013250"},{"key":"186_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"SAS","author":"B Cook","year":"2005","unstructured":"Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: SAS. Lecture notes in computer science, vol 3672. Springer, Berlin, pp 87\u2013101"},{"key":"186_CR13","first-page":"415","volume-title":"PLDI","author":"B Cook","year":"2006","unstructured":"Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: PLDI. ACM, New York, pp 415\u2013426"},{"key":"186_CR14","first-page":"1","volume-title":"Workshop on advances in verification","author":"D Dams","year":"2000","unstructured":"Dams D, Gerth R, Grumberg O (2000) A\u00a0heuristic for the automatic generation of ranking functions. In: Workshop on advances in verification, pp 1\u20138"},{"key":"186_CR15","series-title":"Electronic notes in theoretical computer science","first-page":"85","volume-title":"INFINITY","author":"E Encrenaz","year":"2009","unstructured":"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\u2013103"},{"key":"186_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-642-27705-4_21","volume-title":"VSTTE","author":"S Falke","year":"2012","unstructured":"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\u2013277"},{"key":"186_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-540-30494-4_15","volume-title":"FMCAD","author":"E Giunchiglia","year":"2004","unstructured":"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\u2013213"},{"key":"186_CR18","first-page":"28","volume-title":"Formal methods in computer-aided design (FMCAD)","author":"A Griggio","year":"2011","unstructured":"Griggio A (2011) Effective word-level interpolation for software verification. In: Formal methods in computer-aided design (FMCAD). IEEE Press, New York, pp 28\u201336"},{"key":"186_CR19","first-page":"35","volume-title":"PLDI","author":"S Horwitz","year":"1988","unstructured":"Horwitz S, Reps TW, Binkley D (1988) Interprocedural slicing using dependence graphs. In: PLDI. ACM, New York, pp 35\u201346"},{"key":"186_CR20","series-title":"Electronic notes in theoretical computer science","first-page":"45","volume-title":"Workshop on bounded model checking (BMC\u201906)","author":"T Jussila","year":"2007","unstructured":"Jussila T, Biere A (2007) Compressing BMC encodings with QBF. In: Workshop on bounded model checking (BMC\u201906). Electronic notes in theoretical computer science, vol 174. Elsevier, Amsterdam, pp 45\u201356"},{"key":"186_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"SAT","author":"T Jussila","year":"2007","unstructured":"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\u2013214"},{"key":"186_CR22","volume-title":"SMT workshop at IJCAR","author":"G Kov\u00e1sznai","year":"2012","unstructured":"Kov\u00e1sznai G, Fr\u00f6hlich A, Biere A (2012) On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: SMT workshop at IJCAR"},{"key":"186_CR23","first-page":"212","volume-title":"Design automation conference (DAC)","author":"G Parthasarathy","year":"2004","unstructured":"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\u2013217"},{"key":"186_CR24","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"VMCAI","author":"A Podelski","year":"2004","unstructured":"Podelski A, Rybalchenko A (2004) A\u00a0complete method for the synthesis of linear ranking functions. In: VMCAI. Lecture notes in computer science, vol 2937. Springer, Berlin, pp 239\u2013251"},{"key":"186_CR25","first-page":"32","volume-title":"LICS","author":"A Podelski","year":"2004","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: LICS. IEEE Press, New York, pp 32\u201341"},{"key":"186_CR26","series-title":"Lecture notes in computer science","first-page":"245","volume-title":"PADL","author":"A Podelski","year":"2007","unstructured":"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\u2013259"},{"key":"186_CR27","first-page":"92","volume-title":"Sprawozdanie z I kongresu metematyk\u00f3w slowia\u0144skich","author":"M Presburger","year":"1930","unstructured":"Presburger M (1930) \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Sprawozdanie z I kongresu metematyk\u00f3w slowia\u0144skich, Warsaw, 1929, pp 92\u2013101."},{"key":"186_CR28","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"LPAR","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer P (2008) A\u00a0constraint sequent calculus for first-order logic with linear integer arithmetic. In: LPAR. Lecture notes in computer science, vol 5330. Springer, Berlin, pp 274\u2013289"},{"key":"186_CR29","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A (1986) Theory of linear and integer programming. Wiley, New York"},{"key":"186_CR30","first-page":"1","volume-title":"STOC","author":"LJ Stockmeyer","year":"1973","unstructured":"Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time (preliminary report). In: STOC. ACM, New York, pp 1\u20139"},{"issue":"5","key":"186_CR31","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1145\/367236.367286","volume":"3","author":"P Wegner","year":"1960","unstructured":"Wegner P (1960) A technique for counting ones in a binary computer. Commun ACM 3(5):322","journal-title":"Commun ACM"},{"key":"186_CR32","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"CM Wintersteiger","year":"2013","unstructured":"Wintersteiger CM, Hamadi Y, de Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42:3\u201323","journal-title":"Form Methods Syst Des"},{"key":"186_CR33","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"CAV","author":"H Yang","year":"2008","unstructured":"Yang H, Lee O, Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW (2008) Scalable shape analysis for systems code. In: CAV. Lecture notes in computer science, vol 5123. Springer, Berlin, pp\u00a0385\u2013398"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0186-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0186-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0186-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:53Z","timestamp":1559253953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0186-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,21]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["186"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0186-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,21]]}}}