COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Verification for free: using K to build a theorem prover for any language

## Verification for free: using K to build a theorem prover for any languageAdd to your list(s) Download to your calendar using vCal - Bruce Collie, Runtime Verification
- Friday 07 October 2022, 14:00-15:00
- SS03.
If you have a question about this talk, please contact Jamie Vicary. The K Framework allows you to produce all your language’s tools (parser, fast concrete interpreter, symbolic execution, ...) from a single definition of its syntax and operational semantics. To do so, we rely on a consistent internal formalism based on term rewriting. In this talk, I’ll first briefly introduce the K language and explain how we compile arbitrary language definitions down to this internal formalism. Perhaps the most important tool that K offers is deductive verification.
In the second
part of my talk, I’ll give an overview of the underlying modal logic for
this capability
(matching-mu logic), along with the kinds of formulae we’re interested
in proving in it.
From here, we can join the dots back to the terms generated by the K
compiler, and
derive a full formal verification toolchain for This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- SS03
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsGuy Emerson's list Exam Passing Material MedSin Cambridge## Other talksWhen do we forgive a friend? Metal Pad Roll Instability in Two or Three Layers of Liquid Metals Designing the BEARS (Both Ears) Virtual Reality Training Package to Improve Spatial Hearing in Young People with Bilateral Cochlear Implant Milner Seminar Series - October 2022 A Crossroad between Statistical Mechanics, PDE-Theory, Neural Networks and Machine Learning Avos: Looking back 15 years: the technological changes leading to the Zoom Cat Lawyer |