Formal Verification of Bit-Vector Invertibility Conditions in Coq

DOI10.1007/978-3-031-43369-6_3MaRDI QIDQ6496617

Cesare Tinelli, Arjun Viswanathan, Yoni Zohar, Clark Barrett, Burak Ekici

Publication date: 3 May 2024

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Hammer for Coq: automation for dependent type theory
• Towards satisfiability modulo parametric bit-vectors
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Towards bit-width-independent proofs in SMT solvers
• From Sets to Bits in Coq
• Theorem Proving in Higher Order Logics
• Equations: A Dependent Pattern-Matching Compiler
• Solving quantified bit-vectors using invertibility conditions

This page was built for publication: Formal Verification of Bit-Vector Invertibility Conditions in Coq