Towards satisfiability modulo parametric bit-vectors

DOI10.1007/s10817-021-09598-9OpenAlexW3173823616MaRDI QIDQ2051567

Clark Barrett, Cesare Tinelli, Aina Niemetz, Andrew Reynolds, Yoni Zohar, Mathias Preiner

Publication date: 24 November 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-021-09598-9

zbMATH Keywords

satisfiability modulo theoriesbit-precise reasoningparametric bit-vectors

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Isabelle/HOL
• VAMPIRE
• z3
• LLVM
• Sledgehammer
• CVC4
• AVATAR
• SMTCoq
• CVC4SY

Cites Work

• Unnamed Item
• Unnamed Item
• Complexity of fixed-size bit-vector logics
• Decision procedures. An algorithmic point of view
• Isabelle/HOL. A proof assistant for higher-order logic
• Experimenting on solving nonlinear integer arithmetic with incremental linearization
• Designing theory solvers with extensions
• On solving quantified bit-vector constraints using invertibility conditions
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Syntax-guided rewrite rule enumeration for SMT solvers
• Towards bit-width-independent proofs in SMT solvers
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Revisiting enumerative instantiation
• Extending Sledgehammer with SMT solvers
• AVATAR: The Architecture for First-Order Theorem Provers
• Efficient E-Matching for SMT Solvers
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• Logics in Artificial Intelligence

This page was built for publication: Towards satisfiability modulo parametric bit-vectors