K Developer Interviewed in Illinois Paper

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.

wired_in_radoi

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.

 

capture
CS article

 

 

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

Capture

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

Runtime Verification seeking a Software Development Engineer

Runtime Verification, Inc is looking for a software engineer 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

RV Inc. to Give Tutorial at Runtime Verification ’16 Conference

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!

2016-05-25--1464206820_1518x728_scrot

Testing K Framework using RV-Predict

This blog post is the beginning of a series of blog posts recording our experience of hunting data races in complex real-world applications using RV-Predict. To start with, we will choose the K framework as our first test subject.

Why the K framework? Well, there are a number of reasons. First of all, it’s a very cool project! Check out its website for a quick introduction. It is also the foundation of our RV-Match product, which aims to provide strong correctness guarantees through formal verification. Therefore, it’s very important that the underlying K Framework is free from bugs including data races. Finally, the K framework is complex. It is written in a combination of Java and Scala and makes use of the Java 8 features extensively. It also takes advantage of many 3rd-party libraries such as Guice, Guava, Nailgun, etc. As a practical race detector, RV-Predict must be able to handle all these aspects gracefully.
Continue reading

Detecting popular data races in Java using RV-Predict

Data races are a common kind of concurrency bug in multithreaded applications. A data race can be defined as two threads accessing a shared memory location concurrently and at least one of the accesses is a write. Data races are notoriously difficult to find and reproduce because they often happen under very specific circumstances. Therefore, you could have a successful pass of the tests most of the time but some test fails once in a while with some mysterious error message far from the root cause of the data race.

Despite all the effort on solving this problem, it remains a challenge in practice to detect data races effectively and efficiently. RV-Predict aims to change this undesired situation. In this blog post, we will summarize some of the most popular kinds of data races in Java and show you how to catch them using RV-Predict. The examples in this post are included in the RV-Predict distribution under the examples/ directory.

Continue reading

Using RV-Predict to track down race conditions

We’ve all had it happen: you write some multithreaded code, but when you run it, it crashes with some kind of error every second or third or hundredth run. The traditional way of trying to debug this problem is very tedious and involves attempting to reproduce the error (difficult) and then tracing the inconsistent state backwards to find the source of the race condition (even more difficult).

Enter RV-Predict. Today I was developing code for RV-Match when I ran into an intermittently occurring NullPointerException in its parser. Instead of trying to reproduce the bug and tracking its behavior backwards, I assumed going in that it was caused by a race condition, and ran RV-Predict on the program. After it crashed, it spat out the following error report: Continue reading