University of Cambridge > Talks.cam > SANDWICH Seminar (Computer Laboratory) > Decision Procedures for Bitvector Reasoning in Lean

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Decision Procedures for Bitvector Reasoning in Lean

Download to your calendar using vCal

If you have a question about this talk, please contact Ariadne Si Suo .

I’ll be giving a broad overview of the decision procedures we have been building for bitvector reasoning in Lean, with both fixed and infinite width. Time permitting, I shall sketch the design and mechanization strategy of the infinite width decision procedure, since the core involves verifying a cute model checking algorithm (k-induction), with games to be played to hook in a SAT solver into the tactic loop.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Seminar room, Sociology Department, Free School Lane Biological Anthropology Easter Term Seminars 2012 Room 251, Helmore Building, Anglia Ruskin University, East Road, CB1 1PT

Other talks

Title to be confirmed Science & the Public in Action: Can and should climate scientists be activists? Precision psychiatry Group Work Talk title TBC The Inaccessible Game
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity