Grigore Roșu

Grigore Roșu (born December 12, 1971) is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in the Information Trust Institute.^[1] He is known for his contributions in Runtime Verification, the K framework,^[2] matching logic,^[3] automated coinduction.^[4], and for founding Runtime Verification, Inc. and Pi Squared, Inc..

Grigore Roșu
Roșu in 2020
Born	(1971-12-12) December 12, 1971 (age 53)
Nationality	Romanian-American
Alma mater	University of Bucharest University of California, San Diego
Known for	Runtime verification K language framework matching logic circular coinduction
Scientific career
Fields	Computer Science
Institutions	University of Illinois at Urbana-Champaign Runtime Verification, Inc. Alexandru Ioan Cuza University Microsoft Research NASA Ames Research Center University of California at San Diego University of Bucharest
Thesis	Hidden Logic (2000)
Doctoral advisor	Joseph Goguen
Website	fsl.cs.illinois.edu/~grosu

Biography

Roșu 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.

After completing his doctorate, he joined NASA in 2000 as a research scientist at the Ames Research Center, where he focused on formal specification and verification of flight and navigation software, coining the term "runtime verification" to enhance the reliability of mission-critical systems.

In 2002, he joined the department of computer science at the University of Illinois at Urbana–Champaign as an assistant professor, later becoming an associate professor in 2008 and a full professor in 2014.

In 2003, Roșu, alongside his student Traian Serbanuta, developed the K framework, providing an intuitive and modular approach to defining formal semantics for programming languages.

He founded Runtime Verification, Inc. in 2010, translating his research into practical applications by collaborating with industry leaders like Boeing and Toyota in the embedded systems domain.

In late 2023, he founded Pi Squared, Inc. as a spin-off from Runtime Verification, aiming to address challenges in programming language interoperability and computational trust.

Awards

• IEEE/ACM most influential paper of the International Conference on Automated Software Engineering (ASE) award in 2016^[5] (for an ASE 2001 paper)^[6]
• Runtime Verification (RV) Test of Time awards in 2018 (for an RV 2001 paper)^[7] and in 2023 (for an RV 2003 paper)^[8]
• ACM distinguished paper awards^[9] at ASE 2008, ASE 2016, and OOPSLA 2016
• Best software science paper award at ETAPS 2002^[10]
• NSF CAREER award in 2005^[11]

• Ad AStra award in 2016^[12]
• Fellow of the Institute of Electrical and Electronics Engineers (IEEE)^[13]
• Fellow of the American Association for the Advancement of Science (AAAS)^[14]

Contributions

Roșu coined the term "Runtime Verification" together with Havelund^[15] as the name of a workshop^[16] started in 2001, aiming at addressing problems at the boundary between formal verification and testing. Roșu and his collaborators introduced algorithms and techniques for parametric property monitoring,^[17] efficient monitor synthesis,^[18] runtime predictive analysis,^[19] and monitoring-oriented programming.^[20]

Roșu created and led the design and development of the K framework,^[2] which is an executable semantic 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,^[21] Java,^[22] JavaScript,^[23] Python,^[24] and Ethereum Virtual Machine^[25] are defined using the K framework.

Roșu introduced matching logic^[3] 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,^[26] typed or untyped lambda-calculi, dependent type systems, separation logic with recursive predicates, rewriting logic,^[27][28] Hoare logic, temporal logics, dynamic logic, and the modal μ-calculus.

Roșu's Ph.D. thesis^[29] proposed circular coinduction^[30] 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,^[31] Isabelle/HOL,^[32] Dafny,^[33] and as part of the CIRC theorem prover.^[34]