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