Runtime Verification seeking experienced C and C++ engineers

Runtime Verification, Inc., (RV) wants to add a Senior Software Engineer to its team that makes verification tools for C and C++ programs.

RV is a growing startup whose software tools help developers make safe, reliable software that runs on automobiles, airplanes, spacecraft, and the blockchain. RV’s verification technology is state-of-the-art, and the company employs leading experts in software engineering and verification.

RV offers great benefits, and its offices have the best views in downtown Urbana.

In the role of Senior Software Engineer, prior experience writing, testing, and debugging multithreaded C or C++ programs is essential. Familiarity with assembly language, operating system internals, embedded systems, or real-time operating systems is highly desirable.

Experience with test-driven development, Java, compiler implementation (especially using LLVM), functional programming, or formal methods is a plus.

In addition to being technically astute, a successful Senior Software Engineer at RV has to be a considerate teammate with good communication skills, and an eager learner with a demonstrable ability to solve problems.

To apply to this position, email a cover letter and résumé to contact (at) (our domain) (dot) com. Use the words “Careers” and “Senior Software Engineer” in the subject.

C11 Fails to Define Data Races Involving Interrupts

Users of our data-race detector for C/C++ programs, RV-Predict/C, frequently tell us at Runtime Verification, Inc., (RV) that they would like to see a variant that detects data races between threads and interrupts in embedded systems. A solitary application thread may share data locations with one or more interrupt service routines (ISRs). Data accesses by the ISRs and the application thread may conflict. The conflicting accesses can lead to unexpected behavior in safety-critical software. Users hope to detect conflicting accesses using runtime verification, and fix their software to avoid the conflicts.

What does it mean to have a "data race" between a thread and an interrupt? We quickly realized at RV that we resorted to a vague analogy between threads and interrupts to define a data race. It was important to produce a formal definition. We are concerned with interrupts only in C programs, so we sought an authoritative definition in the C11 standard. We were surprised when we could not find one!
Continue reading