Grigore Rosu

Grigore Roșu is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in theInformation Trust Institute.He is known for his contributions in runtime verification, K framework, matching logic, and automated coinduction.

Rosu received a B.A. in Mathematics in 1995 and an M.S. in Fundamentals of Computing in 1996, both from the University of Bucharest, Romania, and a Ph.D. in Computer Science in 2000 from the University of California at San Diego.Between 2000 and 2002 he was a research scientist at NASA Ames Research Center.In 2002, he joined the department of computer science at the University of Illinois at Urbana-Champaign as an assistant professor.He became an associate professor in 2008 and a full professor in 2014.

• IEEE/ACM most influential paper of Automate Software Engineering (ASE) award in 2016 (for an ASE 2001 paper)
• Runtime Verification (RV) test of time award (for an RV 2001 paper)
• ACM distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016
• Best software science paper award at ETAPS 2002
• NSF CAREER award in 2005

• Ad AStra award in 2016

Rosu coined the term "runtime verification" together with Havelund as the name of a workshop started in 2001, aiming at addressing problems at the boundary between formal verification and testing.Rosu and his collaboratorsintroduced algorithms and techniques forparametric property monitoring, efficient monitor synthesis,runtime predictive analysis, and monitoring-oriented programming. Rosu has also founded Runtime Verification, Inc., a company aimed at commercializing runtime verification technology.

Rosu created and led the design and development of the K framework, which is an executablesemantic framework where programming languages,type systems, and formal analysis tools are defined using configurations, computations, and rewrite rules.Language tools such as interpreters,virtual machines, compilers, symbolic execution and formal verification tools, are automatically or semi-automatically generated by the K framework.Formal semantics of several known programming languages, such as C, Java, JavaScript, Python, and Ethereum Virtual Machine are defined using the K framework.

Rosu introduced matching logic as a foundation for the K framework and for programming languages,specification, and verification. It is as expressive as first-order logic plus mathematical induction,and uses a compact notation to capture, as syntactic sugar, several formal systems of critical importance, such as algebraic specification and initial algebra semantics, first-order logic with least fixed points, typed or untyped lambda-calculi,dependent type systems,separation logic with recursive predicates, rewriting logic, Hoare logic, temporal logics,dynamic logic, and modal μ-calculus.

Rosu's Ph.D. thesis proposed circular coinduction as an automation of coinduction in the context of hidden logic.This was further generalized into a principle that unifies and automates proofs by both induction and coinduction, and has been implemented in Coq, Isabelle/HOL, Dafny, and as part of the CIRC theorem prover.