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

DOI10.1007/978-3-030-81688-9_7zbMath1493.68387OpenAlexW3183490041MaRDI QIDQ832260

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

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)

Uses Software

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

Cites Work

• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Fast machine words in Isabelle/HOL
• DRAT-based bit-vector proofs in CVC4
• SMT proof checking using a logical framework
• LCF-Style Bit-Blasting in HOL4
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
• Tools and Algorithms for the Construction and Analysis of Systems
• Efficient verified (UN)SAT certificate checking

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