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

DOI10.1007/978-3-662-48899-7_24zbMATH Open1471.68143OpenAlexW2293687462MaRDI QIDQ3460065FDOQ3460065

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

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

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)

Cited In (10)

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

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)