The K Framework provides extensive support for writing and validating formal semantics of programming languages, and using these semantics to execute, analyze, and even verify programs. We are part of a new joint effort to advance the implementation of the K framework - and we are now hiring for this project. The organizations involved are
The Ethereum Virtual Machine (EVM) has been recently given a complete formal semantics using the K framework, as part of the open source KEVM project. The effort is described in detail in the KEVM technical report. The aim of the KEVM project is to develop a suite of formal analysis tools for smart contracts based on the formal semantics of the EVM. In other words, the only trust base for these tools will be the public EVM semantics, which is the best we can hope for. The KEVM team currently consists of researchers and developers at Runtime Verification and in the Formal Systems Laboratory at the University of Illinois, and the project is being partially funded by IOHK.
While defining the formal semantics of EVM in K, there were moments when we asked ourselves "Why did they do it this way?" Also, while verifying smart contracts using the semantics, we found some of the design choices made by the EVM designers questionable; if nothing else, they make verification harder. We have decided to then collect our thoughts during the semantic definition process and during verification of smart contracts after. They were bundled together with the KEVM definition, under issues.md. Here we restate them so you can find them all in one place in order to express your thoughts. Maybe it is not too late to re-design the EVM, this time with formal semantics and mathematical rigor in mind. If the blockchain technology is here is stay, then we should better build it on the most solid foundation that we can.
John Regher's blog is a great source for anyone concerned about undefined behavior in C programs. The latest installment Undefined Behavior in 2017, written jointly with Pascal Cuoq, reviews the state of popular tools for detecting important categories of undefined behavior, and describes a new tool tis-interpreter that they have been working with.
At Runtime Verification we are big proponents of dynamic program analysis and rigorous error detection, so we were excited to hear of another tool following a similar approach to our own undefined-behavior checker, RV-Match(which is the commercial continuation of the academic kcc tool). We tested the most recent available version of tis-interpreter against RV-Match. With roots in the Frama-C verification project, we would hope tis-interpreter is faithful to the C standard - or become concerned that Frama-C could "prove" wrong code correct. We found that tis-interpreter detects many fewer errors than RV-Match, and has missing or incorrect implementations of several language features and almost all library functions. On the positive side, their examples revealed a few errors in RV-Match, which we have now fixed. We will update this post for improvements in tis-interpreter.
Runtime Verification, Inc is looking for two new software engineers to work on our family of products. We are a start-up based in Urbana, Illinois, less than 15 walk minutes away from the Computer Science Department at the University of Illinois in Urbana-Champaign (UIUC), which is in the top 5 schools in Computer Science in the United States and the top 1-2 schools in the domains of software engineering, formal methods and programming languages. Continue reading →
A local paper, the News-Gazette interviewed Cosmin Radoi. He has contributed to the K framework for several years while studying at UIUC with Grigore Rosu. Cosmin's latest project Kale uses the rewriting approach of the K framework to suggest program transformations and improvements, instead of using it to examine how programs execute according to a formal language semantics, as in RV-Match and much of the academic work with K. We wish Cosmin well in his own efforts to provide powerful software development tools.
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.
Runtime Verification Inc. is going to be presenting an exciting tutorial at the RV'16 conference, featuring all of our current tools and technologies and their practical and creative uses and applications.
If you are new (or a veteran) to runtime verification technology, we invite you to join and learn about what RV Inc.'s tools can do for your codebase, today. We look forward to seeing you in sunny, beautiful Madrid!
Our founder was interviewed by the University of Illinois' Click Magazine about how the RV technology can make cars safer. Below is the article they published that features our RV-ECU project funded by the NSF SBIR program (see pages 38-39):