Decision Procedures for Bitvector Reasoning in Lean
Add to your list(s)
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.
|