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:
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:
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.
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.