BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Decision Procedures for Bitvector Reasoning in Lean - Siddharth Bh
 at (University of Cambridge)
DTSTART:20250123T170000Z
DTEND:20250123T180000Z
UID:TALK224860@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:I’ll be giving a broad overview of the decision procedures w
 e have been building for bitvector reasoning in Lean\, with both fixed and
  infinite width. Time permitting\, I shall sketch the design and mechaniza
 tion strategy of the infinite width decision procedure\, since the core in
 volves verifying a cute model checking algorithm (k-induction)\, with game
 s to be played to hook in a SAT solver into the tactic loop.\n\nNote: work
  done in collaboration with the wider Lean community\, and effort led by t
 he Lean FRO: Henrik Boving\, Kim Morrison\, and Leo de Moura.\n\n=== Hybri
 d talk ===\n\nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pw
 d=SELTNkOcfVrIE1IppYCsbooOVqenzI.1\n\nMeeting ID: 871 4336 5195\n\nPasscod
 e: 541180
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR