BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification for free: using K to build a theorem prover for any l
 anguage - Bruce Collie\, Runtime Verification
DTSTART:20221007T130000Z
DTEND:20221007T140000Z
UID:TALK183080@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:The K Framework allows you to produce all your language's tool
 s (parser\,\nfast\nconcrete interpreter\, symbolic execution\, ...) from a
  single definition\nof its\nsyntax and operational semantics. To do so\, w
 e rely on a consistent internal\nformalism based on term rewriting. In thi
 s talk\, I'll first briefly\nintroduce the K\nlanguage and explain how we 
 compile arbitrary language definitions down to\nthis internal formalism.\n
 \nPerhaps the most important tool that K offers is deductive verification.
 \nIn the second\npart of my talk\, I'll give an overview of the underlying
  modal logic for\nthis capability\n(matching-mu logic)\, along with the ki
 nds of formulae we're interested\nin proving in it.\n From here\, we can j
 oin the dots back to the terms generated by the K\ncompiler\, and\nderive 
 a full formal verification toolchain for _any_ language.
LOCATION:SS03
END:VEVENT
END:VCALENDAR