lazybvtoint at the SMT Competition 2020
Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Notzli, Andrew Reynolds,, Clark Barrett
TL;DR
LazyBVtoInt is a new SMT solver prototype designed for the QF_BV logic, aiming to participate in the SMT Competition 2020's incremental and non-incremental tracks.
Contribution
Introduces LazyBVtoInt, a novel SMT solver prototype tailored for QF_BV logic, with potential improvements in solving efficiency.
Findings
Participated in SMT Competition 2020
Demonstrated capability in incremental and non-incremental tracks
Showed competitive performance in QF_BV logic solving
Abstract
lazybvtoint is a new prototype SMT-solver, that will participate in the incremental and non-incremental tracks of the \qfbv logic.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCryptography and Data Security · Logic, programming, and type systems · Formal Methods in Verification