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.

[19] 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.

Formal semantics of several known programming languages, such as C,[20] Java,[21] JavaScript,[22] Python,[23] and Ethereum Virtual Machine[24] 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.

This was further generalized into a principle that unifies and automates proofs by both induction and coinduction, and has been implemented in Coq,[30] Isabelle/HOL,[31] Dafny,[32] and as part of the CIRC theorem prover.