BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Atticus Kuhn (University of Cambridge\, Department of Computer Sci
 ence)
DTSTART:20260123T170000Z
DTEND:20260123T173000Z
DTSTAMP:20260420T025340Z
UID:LT2026/46
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/46/">
 Verification of model-checking techniques in Lean</a>\nby Atticus Kuhn (Un
 iversity of Cambridge\, Department of Computer Science) as part of Lean To
 gether 2026\n\n\nAbstract\nVardi 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 syst
 ems. 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.\n
LOCATION:https://researchseminars.org/talk/LT2026/46/
END:VEVENT
END:VCALENDAR