CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
From MaRDI portal
Publication:832260
DOI10.1007/978-3-030-81688-9_7zbMATH Open1493.68387OpenAlexW3183490041MaRDI QIDQ832260FDOQ832260
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
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Isabelle/HOL. A proof assistant for higher-order logic
- SMT proof checking using a logical framework
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Tools and Algorithms for the Construction and Analysis of Systems
- Efficient verified (UN)SAT certificate checking
- Fast machine words in Isabelle/HOL
- DRAT-based bit-vector proofs in CVC4
- LCF-style bit-blasting in HOL4
- Fine grained SMT proofs for the theory of fixed-width bit-vectors
- Title not available (Why is that?)
Cited In (5)
- Fine grained SMT proofs for the theory of fixed-width bit-vectors
- Towards bit-width-independent proofs in SMT solvers
- Formal Verification of Bit-Vector Invertibility Conditions in Coq
- \textsc{CoqCryptoLine}: a verified model checker with certified results
- Certified verification for algebraic abstraction
Uses Software
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)
