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


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.


Youtube interview with Prof Grigore Rosu


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s