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
Positions for professional developers are available at RV, IOHK, and ADSC. The K website has full details on the projects and the available positions.
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.
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.