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 B
 hat (University of Cambridge)
DTSTART:20250120T130000Z
DTEND:20250120T140000Z
UID:TALK226357@talks.cam.ac.uk
CONTACT:Ariadne Si Suo
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. 
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR