Grigore Rosu

Grigore Rosu is a Professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign, where he leads the Formal Systems Laboratory (FSL). He is also the founder and President of Runtime Verification, Inc. (2010) and Pi Squared, Inc. (2023). Rosu's research bridges theoretical foundations and practical system development in formal methods, software engineering, and programming languages.

His academic journey includes a Ph.D. in Computer Science (2000, University of California at San Diego), an M.S. in Fundamentals of Computing (1996, University of Bucharest), and a B.A. in Mathematics (1995, University of Bucharest). Prior to UIUC, he worked as a Research Scientist at NASA Ames Research Center (2000-2002) and took a sabbatical at Microsoft Research (2008).

Rosu's research has shaped the field of runtime verification (coined with Klaus Havelund in 2001), introduced the K framework (2003) for executable semantics, and pioneered matching logic as a unifying foundation for formal reasoning. His work spans automated coinduction, monitoring-oriented programming, and formal semantics for C, Java, JavaScript, Python, and the Ethereum Virtual Machine. He has received numerous awards, including the NSF CAREER, Dean's Award for Excellence in Research, and IEEE/ACM Most Influential Paper Award.

Scientific Honors:

• AAAS Fellow (2022)
• IEEE Fellow (2021)
• Test of Time Awards (RV 2001, 2018; RV 2003, 2023)
• Distinguished Paper Awards (ASE 2008, ASE 2016, OOPSLA 2016, ETAPS 2002)
• NSF CAREER Award (2005)
• Dean's Award for Excellence in Research (2014)

Rosu teaches advanced courses in programming language design, formal semantics, and blockchain technology. His innovations have been commercialized through Runtime Verification, Inc., serving clients like NASA, Boeing, Toyota, and blockchain entities such as Ethereum Foundation.