Intro

“Formal semantics can avoid stupid errors, for example, programs that give different results for different for different compilers version.” – Prof Grigore Rosu.

K-framework

K-framework, from the Runtime Verification team, and by the group of Prof Grigore Rosu at University Urbana Campaign.

A Meta-language

K-framework is a language to describe other languages.

Smart-contract utilization

His main idea is to use the k-framework to verify smart contracts.

REFs

Youtube interview with Prof Grigore Rosu