Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic

DOI10.1007/978-3-030-45190-5_5OpenAlexW3016942815MaRDI QIDQ5039504

Andy King, Takamasa Okudono

Publication date: 13 October 2022

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

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)

Uses Software

• BLAST
• KRATOS
• MathSAT5
• FOCI

Cites Work

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

This page was built for publication: Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic