CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver

DOI10.1007/978-3-030-81688-9_7MaRDI QIDQ832260zbMATHOpenAlexFDO

Authors Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Publication date 25 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-81688-9_7

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

• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Fine grained SMT proofs for the theory of fixed-width bit-vectors
• DRAT-based bit-vector proofs in CVC4
• Validating QBF Validity in HOL4
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Cites work

• scientific article; zbMATH DE number 7378548 (Why is no real title available?)
• DRAT-based bit-vector proofs in CVC4
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Efficient verified (UN)SAT certificate checking
• Fast machine words in Isabelle/HOL
• Fine grained SMT proofs for the theory of fixed-width bit-vectors
• Isabelle/HOL. A proof assistant for higher-order logic
• LCF-style bit-blasting in HOL4
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• SMT proof checking using a logical framework
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(5)

• Formal Verification of Bit-Vector Invertibility Conditions in Coq
• Towards bit-width-independent proofs in SMT solvers
• \textsc{CoqCryptoLine}: a verified model checker with certified results
• Certified verification for algebraic abstraction
• Fine grained SMT proofs for the theory of fixed-width bit-vectors

Describes a project that uses

Uses Software

• ACL2
• Isabelle/HOL
• CLSAT
• CVC4
• CBMC
• RELIC
• DRAT-trim
• CaDiCaL
• GitHub
• Paracooba
• Kissat

This page was built for publication: CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver

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