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
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.
RV-Match now supports execution of applications containing x86_64 inline assembly. If you have a program that contains inline assembly, you can compile it with kcc like any other C program and we will compile the functions containing inline assembly with gcc and execute them directly the same way we handle any other native code which we do not have C source for. As a result of this, the ability to detect undefined behavior in that function is eliminated, but it allows you to analyze complex applications which contain some code in inline assembly which you do not want to translate into C source.
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.
Users of our data-race detector for C/C++ programs, RV-Predict/C, frequently tell us at Runtime Verification, Inc., (RV) that they would like to see a variant that detects data races between threads and interrupts in embedded systems. A solitary application thread may share data locations with one or more interrupt service routines (ISRs). Data accesses by the ISRs and the application thread may conflict. The conflicting accesses can lead to unexpected behavior in safety-critical software. Users hope to detect conflicting accesses using runtime verification, and fix their software to avoid the conflicts.
What does it mean to have a "data race" between a thread and an interrupt? We quickly realized at RV that we resorted to a vague analogy between threads and interrupts to define a data race. It was important to produce a formal definition. We are concerned with interrupts only in C programs, so we sought an authoritative definition in the C11 standard. We were surprised when we could not find one! Continue reading →
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 →
Not long ago, one of our customers came to us confused about an analysis report on a simple program their company used internally to assess knowledge of C. Among the code they sent us was something like the following three lines:
They assumed that this code should be free from defects, and thought that possibly the two defects we reported were incorrect. Let's take a look at the error reports that result when we insert these lines into a simple program and execute them: 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.