Runtime Verification Inc is an American startup with a global presence, applying formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain. We work with infrastructure builders to provide testing and verification services and tools.
The company was founded in 2010 by pioneers in the academic field and it gained a select roster of clients in the embedded systems space (NASA, Boeing, Toyota, Denso, NSF, DARPA) and the blockchain (Algorand, Cosmos, MultiversX, Ethereum, Gnosis, IOHK, Maker, PlatON, Polkadot, Tezos, and Uniswap), among many others.
Located between Urbana (the home of the University of Illinois) and its sister city of Champaign, our headquarter is roughly 2.5 hours South of Chicago, 2 hours West of Indianapolis, and 3 hours North of St. Louis. In 2018, Champaign scored the #1 spot in the Best Cities for Recent College Grads ranking, and #2 overall (out of 42 communities) in the Silicon Prairie region.
Our mission is accessible trustworthy computing. We accomplish it by generating correct-by-construction implementations and tools automatically, from their specifications. One of our unique technologies is K, a semantic framework for design, implementation and formal reasoning. K allows language designers to formally define their language using an intuitive and attractive notation, and generate for free the implementations and the analysis tools for that defined language.
Our symbol, the two drops (blue and yellow), represent the specification and the implementation. During verification we prove that the two are tightly connected, therefore two rigidity points (RV-Match). For dynamic analysis (RV-Predict and RV-Monitor) some aspects get verified, but not all the implementation, therefore one rigidity point. The two drops mirror each other, but not perfectly.
RV-Match
Get to market faster, increase code portability, and save on development and debugging with the most advanced and precise semantics-based bug finding tool.
RV-Monitor
Automatically check your code for compliance with the Java API, or check custom specifications of your choice.
RV-Predict
RV-Predict automatically detects the rarest and most difficult data races in your Java and C/C++ code, saving on development and testing effort with the most precise race finder available.
Bruce Collie is a software engineer and former PhD student at the University of Edinburgh, where he worked on compilers and program synthesis research. Prior to that, he received his BA from the University of Cambridge and worked on runtime temporal logic support for C programs. Outside of work, he likes to cook, run and play rugby.
Everett Hildenbrandt is a formal modeling engineer and product owner at RV. His interests include automated system analysis via symbolic model checking, rigorous software development via carefully designed development practices, and applying these techniques to the software used in the other sciences (eg. physics, biology). He strongly believes that programming languages and system description languages should not be put together in an ad-hoc manner, rather they should be carefully designed using state of the art language-building tools.
Raoul Schaffranek studied Computer Science at RWTH Aachen University, Germany, where he obtained B.Sc. and M.Sc. degrees. He wrote his master thesis about compositional modeling and fully automated verification of distributed systems and formalized his findings with the Isabelle proof assistant. Before joining RV, Raoul worked for more than eight years as a software engineer for the German software company graphodata AG. Raoul considers programming a human-centric rather than machine-centric activity, and he firmly believes that we should build modern programming languages and verification tools upon this perspective.
Rikard Hjort is researching formal methods for developing high-assurance smart contracts for blockchains. He worked on formalizing WebAssembly in K, and now uses KWasm to verify smart contracts written in WebAssembly. He has an M.Sc. in Computer Science from the Chalmers University of Technology, Sweden. He was an intern at Google in 2016 and 2017, and studied at the University of Tokyo in 2017-2018 where he combined his research on blockchains with studying coercion-resistant voting protocols.
Yliès Falcone is a pioneer of the runtime verification field, with more than 15 years of contributions to formal methods and software engineering. He is passionate about designing, implementing, integrating and delivering methods and tools that help guarantee programs are safe and secure. Yliès firmly believes that runtime monitoring is key to achieving this goal. He was a visiting research scholar at many institutions around the globe, working with talented and friendly colleagues who shaped the monitoring discipline. He enjoys solving problems, turning ideas into solutions and mentoring engineers. Yliès also holds an Associate Professor position at Univ. Grenoble Alpes, France.
