Sökning: onr:"swepub:oai:DiVA.org:mdh-54409" >
Interpolating bit-v...
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
-
- Backeman, Peter (författare)
- Mälardalens högskola,Inbyggda system,Mälardalen Univ, Västerås, Sweden.
-
- Rümmer, Philipp, 1978- (författare)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Zeljic, Aleksandar (författare)
- Stanford Univ, Stanford, CA 94305 USA.
-
(creator_code:org_t)
- 2021-05-12
- 2021
- Engelska.
-
Ingår i: Formal methods in system design. - : SPRINGER. - 0925-9856 .- 1572-8102. ; 57:2, s. 121-156
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://link.springe...
-
https://uu.diva-port... (primary) (Raw object)
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bit-vector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider. We also incorporate a method for handling concatenations and extractions of bit-vector efficiently.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Bit-vectors
- Interpolation
- Quantifier elimination
- Presburger arithmetic
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas