This week, we will have Pieter Collins, from Maastricht University, visiting us for a few days. Pieter will give a seminar next Tuesday (see title and abstract below).

Title

Verified Verification - Rigorous Numerics and Model Checking in Rocq/Lean

Model checking tools aim to verify whether a dynamic system satisfies its specification. Since mistakes in the methods or bugs in the implementation could cause a system to be erroneously verified as correct, it is important to also verify the model-checker, which we can do using a proof assistant such as Rocq or Lean. In this talk, I will describe a road-map to such a checker, and work towards implementing the required rigorous numerical methods and systems theory in the “VerifiedCalculus” library.