BucharestFP invites you to talk about the contributions to the world of formal verification, using the open-source K framework. RSVP and let’s meet on March 10, starting at 18:45!
About the event
This talk will be a brief introduction to K by example and by comparison with Haskell. We’ll start by discussing the programming language IMP, with some demonstrations of programs in this language. Then we’ll show how to make an interpreter for this language in Haskell, including a parser and evaluation engine.
Finally, we’ll transition to a K interpreter for this language, and show how in addition to an interpreter, K gives a symbolic execution engine that can be used to do program verification. Any remaining time can be used to try things live and for further discussions about what verification is.
About the speaker
Everett Hildenbrandt is a Formal Modelling Engineer and Product Owner at Runtime Verification, Inc (a software quality assurance firm). He currently works mostly with KEVM, a K semantics of the Ethereum Virtual Machine (EVM) https://github.com/kframework/evm-semantics. He believes strongly in a semantics-first approach to designing and building the tooling around programming languages.
- 18:45 — 19:00 Welcome
- 19:00 — 20:00 Everett Hildenbrandt — Side-by-side implementation of an IMP language in K and Haskell
- 20:00 — 21:00 Networking