skip to content

Department of Computer Science and Technology

Monday, 11 March, 2024 - 13:05 to 13:55
Bruce Collie
FW26, William Gates Building

Runtime Verification provides formal verification, auditing and tool development services focused on programming language semantics. At the heart of our approach is the K Framework, a programming language and tool ecosystem that allows for tooling (e.g. a parser, symbolic execution engine, or a theorem prover) to be extracted automatically from a single description of a language’s syntax and operational semantics.

In this talk, I’ll cover the K Framework from a technical perspective: how can these tools be built to be both language-agnostic and practical? Then, I’ll talk a bit about how we’ve built a commercial offering on top of K: what approaches are useful for providing formal verification in the real world?

Some catering will be provided

Seminar series: 
Technical Talks

Upcoming seminars