Formal Verification of Bit-Vector Invertibility Conditions in Coq

DOI10.1007/978-3-031-43369-6_3MaRDI QIDQ6496617zbMATH OpenFDO

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

Publication date 3 May 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-43369-6_3

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• Solving quantified bit-vectors using invertibility conditions
• Fine grained SMT proofs for the theory of fixed-width bit-vectors
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Towards bit-width-independent proofs in SMT solvers
• On solving quantified bit-vector constraints using invertibility conditions

Cites work

• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Equations: a dependent pattern-matching compiler
• From Sets to Bits in Coq
• Hammer for Coq: automation for dependent type theory
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 7178362 (Why is no real title available?)
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Solving quantified bit-vectors using invertibility conditions
• Theorem Proving in Higher Order Logics
• Towards bit-width-independent proofs in SMT solvers
• Towards satisfiability modulo parametric bit-vectors

Cited in

(1)

• Invertibility conditions for floating-point formulas

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

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