This paper describes a new proof tool for deciding bit-vector problems in HOL4. The approach is based on "bit-blasting", wherein word expressions are mapped into propositional formulas, which are then handed to a SAT solver. Significantly, the implementation uses the LCF approach, which means that the soundness of the tool is guaranteed by the soundness of HOL4's logical kernel. © 2011 Springer-Verlag.
CITATION STYLE
Fox, A. C. J. (2011). LCF-style bit-blasting in HOL4. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6898 LNCS, pp. 357–362). https://doi.org/10.1007/978-3-642-22863-6_26
Mendeley helps you to discover research relevant for your work.