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, 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
Here is an article analyzing the DAO attack, written by Philip Daian, an RV employee expert in security currently completing his PhD at Cornell: Analysis of the DAO Exploit.
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):
This is our second post on hunting data races in real-world applications using RV-Predict. As promised in our previous post, we are now going after the big-name projects! This time our test subject is Apache Tomcat, which is arguably the most popular Java application server at the time being.
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.
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
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
It would appear that Mac OS X's copy of string.h is invalid.
It declares strcpy as
char *strcpy(char *, const char *);
But the C standard declares it as
char *strcpy(char * restrict, const char * restrict);
These two types are actually incompatible with each other according to the C standard, and a function that is declared more than once in different translation units with different declarations is considered undefined behavior. Thus, any correctly conforming C library will cause any code that includes string.h to be undefined.