Verification of model-checking techniques in Lean
Atticus Kuhn (University of Cambridge, Department of Computer Science)
Fri Jan 23, 17:00-17:30 (4 weeks ago)
Abstract: Vardi proved that model-checking LTL properties can be witnessed by the existence of a certain ranking function. We have formalised Vardi's result in Lean4 for both finite and infinite-state systems. Additionally, we show how the Lean formalisation can be extended to Neural Ranking Functions (NRFs), a modern technique that allows candidate ranking functions to be machine-generated.
logic in computer sciencemathematical softwareMathematics
Audience: researchers in the discipline
| Organizer: | Jireh Loreaux* |
| *contact for this listing |
Export talk to