Our team is dedicated to bringing you the most precise
analysis tools from the latest research.
Grigore Rosu is a computer science professor at the University of Illinois (UIUC), where he leads the Formal Systems Laboratory (FSL). Before joining UIUC, Grigore was a scientist at NASA, where he coined the term runtime verification together with his NASA colleagues. He was offered the NSF CAREER award, the UIUC outstanding junior award, and the Dean's award for excellence in research. He founded Runtime Verification, Inc., in 2010, as a vehicle to promote and incorporate the new and promising runtime verification technology into robust and practical commercial-grade products.
Jed Taylor is the Chief Operating Offer of Runtime Verification (RV). In addition to his role at RV he is a Director at the Technology Entrepreneur Center at UIUC and serves as an Entrepreneur in Residence at EnterpriseWorks, the UIUC startup incubator. Jed has successfully taken several software products to market and has helped start several companies in the Urbana-Champaign area licensing university technology, including Pattern Insight, an NSF SBIR funded company that was acquired by VMWare in 2012.
Dwight Guth is the lead software engineer on the RV-Match project at Runtime Verification, Inc. He received an M.S. in computer science from UIUC in 2013 and a B.S. in computer science and mathematics from Purdue in 2011. His Master's thesis is related to an operational semantics of Python 3 developed using the same technology that ultimately powers RV-Match. Coming from extensive industry experience in software engineering, programming language design, and software verification, he is developing RV-Match from a basic prototype to a fully featured tool capable of analyzing large C applications for undefined behavior and functional correctness.
David Young is a principal embedded engineer at RV, Inc., and the product manager for RV-Predict. David has built networked products based on embedded NetBSD for about 15 years. His work experience covers protocol design and implementation, device drivers, multi-threaded TCP/IP implementation, and ad hoc wireless networks. David is passionate about the pitfalls and potential in human-computer interaction. David got his B.S. in computer science from Cornell University. RV, Inc. makes tools David wishes he could have used for the past decade and a half.
Brandon Moore is a senior software engineer at Runtime Verification, Inc. working primarily on RV-Match. Brandon completed his Ph.D. at UIUC in 2016, working with Grigore to develop formal verification techniques which require only a language definition like those used by RV-Match to verify programs against specific implementations or versions of a programming language. Before UIUC he worked at Yahoo! Inc. on latency-critical servers. Brandon received his B.S. in computer science and in mathematics at Caltech in 2005.
Traian Florin Șerbănuță is a professor of computer science at the University of Bucharest (UNIBUC). Prior to joining UNIBUC, Traian completed his Ph.D. at UIUC in 2010, working with Grigore on the first prototype of the K Framework, which serves as a basis for the RV-Match project. Traian is also involved in the RV-Predict project, for which he designed the initial maximal causal model.
Chris Hathhorn is a senior software engineer on the RV-Match project. He has 10 years of software verification experience in both industry and academia. Currently he is a Ph.D. student in computer science at the University of Missouri and received a B.S. in computer science from UIUC in 2007.
Virgil Nicolae Șerbănuță is a senior software engineer on the RV-Predict and RV-Match projects. Prior to joining Runtime Verification Inc., Virgil received a Ph.D. in Computer Science from University of Bucharest, and worked for 10 years at Google Inc. on projects like Google Maps and Google Timeline. His work experience includes parallel data processing, human query interpretation, and data analysis.
Yilong Li is a Ph.D. student in Computer Science at Stanford University, advised by Professor John Ousterhout. He is also part of the RAMCloud research group and Platform Lab. He is interested in a wide range of topics in software systems, including operating systems, storage systems, programming languages and verification. His current research focuses on building high-performance software stack for ultra-low latency datacenters by creating better software abstractions and designing for simplicity. Prior to joining Stanford, Yilong was a senior software engineer at Runtime Verification, working on the RV-Predict project. His work enables RV-Predict to scale to real-world multithreaded applications while running sophisticated maximal predictive analysis under the hood. He received a B.S. in Computer Science from UIUC in 2014, where he worked on various projects on the K framework.
Philip Daian is the head of smart contract strategy at Runtime Verification, Inc. He has worked with runtime verification in various capacities at both the FSL and RV, Inc. He is now pursuing his PhD in Computer Science at Cornell University with a concentration in systems, where his intended thesis focuses on smart contract security. He is currently involved in several ongoing research projects on smart contract security, provides audit services to the broader smart contract community, and maintains a blog on related topics.