Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
From MaRDI portal
Publication:3460065
DOI10.1007/978-3-662-48899-7_24zbMath1471.68143OpenAlexW2293687462MaRDI QIDQ3460065
Liana Hadarean, Morgan Deters, Clark Barrett, Cesare Tinelli, Andrew Reynolds
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
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (4)
CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver ⋮ 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
