BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Henrik Böving (Lean FRO)
DTSTART:20250115T160000Z
DTEND:20250115T163000Z
DTSTAMP:20261019T200040Z
UID:LeanTogether2025/16
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2025/16/">Automated Bit-Level Reasoning in Lean 4</a>\nby Henrik Böving (
 Lean FRO) as part of Lean Together 2025\n\n\nAbstract\nThis talk will desc
 ribe bv_decide\, a tactic for solving all fixed-width BitVec goals.\nIt wi
 ll give an overview of the inner workings of bv_decide as well as a perfor
 mance evaluation\, showcasing\nsome applications of bv_decide to real worl
 d problems.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/16/
END:VEVENT
END:VCALENDAR