Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) have announced a joint initiative targeting the full formalization of the Viper smart contract programming language, using the K Framework to create a full formal definition of this research-oriented smart contract programming language. This effort is intended to yield a number of useful tools and artifacts, and to lay the foundation for the future of principled and formally rigorous smart contract development. Today, we are happy to announce the release of our first round of fully formal tools for review to the Ethereum community.
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:
int32_t var = 0xffeeddcc; int32_t var2 = 0x7f000000; var2 <<= 8;
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:
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