Mind the gap: bit-vector interpolation recast over linear integer arithmetic

DOI10.1007/978-3-030-45190-5_5MaRDI QIDQ5039504zbMATH OpenOpenAlexFDO

Authors Takamasa Okudono, Andy King

Publication date 13 October 2022

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-45190-5_5

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Deciding Bit-Vector Arithmetic with Abstraction
• Constraint solving for interpolation
• Constraint Solving for Interpolation
• Interpolating quantifier-free Presburger arithmetic

Cites work

• Affine relationships among variables of a program
• An interpolating theorem prover
• Automatic Abstraction for Congruences
• Constraint solving for interpolation
• Deciding Bit-Vector Arithmetic with Abstraction
• Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Interpolant Generation for UTVPI
• Interpolation and model checking
• Lazy abstraction
• Lazy Abstraction with Interpolants
• Programming Languages and Systems
• Taming the Wrapping of Integer Arithmetic
• The MathSAT5 SMT solver
• The small model property: How small can it be?

Cited in

(3)

• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries
• A lazy and modular approach to int-blasting

Describes a project that uses

Uses Software

• FOCI
• KRATOS
• BLAST
• MathSAT5

This page was built for publication: Mind the gap: bit-vector interpolation recast over linear integer arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5039504)