Automated Bit-Level Reasoning in Lean 4
Henrik Böving (Lean FRO)
15-Jan-2025, 16:00-16:30 (21 months ago)
Abstract: This talk will describe bv_decide, a tactic for solving all fixed-width BitVec goals. It will give an overview of the inner workings of bv_decide as well as a performance evaluation, showcasing some applications of bv_decide to real world problems.
logic in computer sciencemathematical softwareMathematics
Audience: researchers in the discipline
Series comments: Most of the talks from the conference are available on YouTube: www.youtube.com/watch?v=ZPPDktjL1Lw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg
| Organizers: | Jireh Loreaux*, Riccardo Brasca*, Kevin Buzzard* |
| *contact for this listing |
Export talk to