New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)

IELE and K Team Runtime Verification has been recently awarded a research and development contract by IOHK to design a next generation virtual machine and a universal language framework to be used as core infrastructure for future blockchain technologies. The formal analysis and verification technology employed in this project has been developed and improved over more than 15 years of research and development, both in the Formal System Laboratory (FSL) at the University of Illinois at Urbana-Champaign and at Runtime Verification, with generous funding from organisations including NSF, NASA, DARPA, NSA, Boeing, Microsoft, Toyota, and Denso. It is about time that aircraft grade, software analysis technology used for mission critical software gets deployed to smart contracts, the blockchain and cryptocurrencies. The project will be executed by a team of Runtime Verification experts led by Prof. Rosu, who will work closely with students at the University of Illinois, also funded by IOHK, and with IOHK R&D personnel. IELE and K Team Photo, left to right: Daejun Park (PhD student at UIUC, RV intern); Theodoros Kasampalis (PhD student at UIUC, RV intern); Yi Zhang (PhD student at UIUC, RV intern); Traian Serbanuta (RV; screen, left bottom); Grigore Rosu (RV and UIUC; screen, center, taking the picture); Virgil Serbanuta (RV; screen, right bottom); David Young (RV); Brandon Moore (RV); Yiyi Wang (RV); Dwight Guth (RV). Also Chris Hathhorn (RV), who missed picture.

Continue reading

ASE 2001 paper that helped shape the Runtime Verification field got the Most Influential Paper Award

Klaus Havelund and I got the ASE 2016 most influential paper award for a paper we published 15 years ago, in ASE 2001.  That paper is important to me because it turned my interest to the field that we now call "runtime verification" (back then, we didn't know exactly what it was).  Below is a link to an article that the CS Department at UIUC just published about this award.


CS article



14% of SV-COMP’s “Correct Programs” are Undefined!


Last April (2016), I gave a tutorial on K at ETAPS'16 in Eindhoven, Netherlands, where I also demonstrated RV-Match.  During the week that I spent there, I heard several friends and colleagues who were involved with the Competition on Software Verification, SV-COMP, that some of the benchmark's correct programs appear to be undefined.  What?  So some of the assumed-correct C programs that are used to evaluate the best program verifiers in the world are actually wrong programs? Continue reading