Fine grained SMT proofs for the theory of fixed-width bit-vectors

DOI10.1007/978-3-662-48899-7_24MaRDI QIDQ3460065zbMATH OpenOpenAlexFDO

Authors Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters

Publication date 12 January 2016

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.703.6112

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• DRAT-based bit-vector proofs in CVC4
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• Rocket-Fast Proof Checking for SMT Solvers
• SMT proof checking using a logical framework
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver

Cited in

(11)

• Scalable fine-grained proofs for formula processing
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• Formal Verification of Bit-Vector Invertibility Conditions in Coq
• Towards bit-width-independent proofs in SMT solvers
• LCF-style bit-blasting in HOL4
• Rocket-Fast Proof Checking for SMT Solvers
• SMT proof checking using a logical framework
• Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method
• Scalable fine-grained proofs for formula processing
• Flexible proof production in an industrial-strength SMT solver

This page was built for publication: Fine grained SMT proofs for the theory of fixed-width bit-vectors

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