Grigore Roșu
Computer science professor
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]
and automated coinduction.[4]
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. 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.[1]
Awards
- Ad AStra award in 2016[12]
Contributions
Roșu coined the term "runtime verification" together with Havelund[13]
as the name of a workshop[14]
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,[15]
efficient monitor synthesis,[16]
runtime predictive analysis,[17]
and monitoring-oriented programming.[18]
Roșu also founded Runtime Verification, Inc.,
a company aimed at commercializing runtime verification technology.[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.
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,[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. 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,[25]
typed or untyped lambda-calculi,
dependent type systems,
separation logic with recursive predicates, rewriting logic,[26][27]
Hoare logic, temporal logics,
dynamic logic, and the modal μ-calculus.
Roșu's Ph.D. thesis[28] proposed circular coinduction[29]
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,[30]
Isabelle/HOL,[31]
Dafny,[32]
and as part of the CIRC theorem prover.[33]
References
- ^ a b Grigore Rosu's curriculum vitae
- ^ a b
K framework. https://kframework.org
- ^ a b
Matching logic. https://matching-logic.org
- ^
Automated coinduction. https://fsl.cs.illinois.edu/index.php/Circ
- ^
Most influential papers of Automated Software Engineering.
https://ase-conferences.org/Mip.html
- ^
K. Havelund, G. Rosu. 2001, Monitoring Programs Using Rewriting,
Automated Software Engineering (ASE), pp. 135-143.
- ^
Runtime Verification.
https://runtime-verification.org/
- ^
K. Havelund, G. Rosu. 2001, Monitoring Java Programs with Java PathExplorer,
Electronic Notes in Theoretical Computer Science vol. 55(2), pp. 200-217.
- ^
ACM SIGSOFT distinguished paper awards.
https://sigsoft.org/awards/distinguishedPaperAward.html
- ^
European Association for the Study of Science and Technology.
https://easst.aulp.co.uk/awards-to-date
- ^
NSF Award Search: Award#0448501 - CAREER: Runtime Verification and Monitoring.
https://nsf.gov/awardsearch/showAward?AWD_ID=0448501
- ^
Grigore Roșu | Premiile Ad Astra.
https://premii.ad-astra.ro/?p=314
- ^
Klaus Havelund homepage. https://havelund.com/
- ^
International Conference of Runtime Verification. https://runtime-verification.org
- ^
G. Rosu, F. Chen. 2012, Semantics and Algorithms for Parametric Monitoring
Logical Methods in Computer Science (LMCS),
vol. 8(1), pp. 1–47.
- ^
P. Meredith, D. Jin, F. Chen, G. Rosu.
2010, Efficient Monitoring of Parametric Context-Free Patterns
Journal of Automated Software Engineering,
vol. 17(2), pp. 149-180.
- ^
F. Chen, T. Serbanuta, G. Rosu.
2008, jPredictor: A Predictive Runtime Analysis Tool for Java
International Conference on Software Engineering (ICSE),
pp. 221–230.
- ^
Monitoring-Oriented Programming. https://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming
- ^
Runtimve Verification Inc.
- ^
C. Hathhorn, C. Ellison, G. Rosu.
2015,
Defining the Undefinedness of C
In Proceedings of Programming Language Design and Implementation (PLDI),
pp. 336-345.
- ^
D. Bogdanas, G. Rosu.
2015,
K-Java: A Complete Semantics of Java
In Proceedings of Principles of Programming Languages (POPL),
pp. 445-456.
- ^
D. Park, A. Stefanescu, G. Rosu.
2015,
KJS: A Complete Formal Semantics of JavaScript
In Proceedings of Programming Language Design and Implementation (PLDI),
pp. 346-356.
- ^
D. Guth.
2013, M.S. thesis,
A Formal Semantics of Python 3.3
University of Illinois at Urbana-Champaign.
- ^
E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, B. Moore, Y. Zhang, D. Park, A. Stefanescu, G. Rosu.
2018,
KEVM: A Complete Semantics of the Ethereum Virtual Machine
In Proceedings of Computer Security Foundations (CSF),
pp. 204-217.
- ^
Y. Gurevich, S. Shelah.
1985,
Fixed-point extensions of first-order logic
In Proceedings of Foundations of Computer Science (SFCS),
pp. 346-353.
- ^
J. Meseguer.
2012,
Twenty Years of Rewriting Logic
In the Journal of Logic and Algebraic Programming (JLAP),
vol. 81(7-8), pp. 721-781.
- ^
Rewriting Logics and Systems,
https://csl.sri.com/programs/rewriting/
- ^
G. Rosu. 2000,
Ph.D. thesis
Hidden Logic
University of California San Diego.
- ^
G. Rosu, D. Lucanu.
2009, Circular Coinduction: A Proof Theoretical Foundation
In Proceedings of Algebra and Coalgebra in Computer Science (CALCO),
pp. 127-144.
- ^
J. Endrullis, D. Hendriks, M. Bodin.
Circular Coinduction in Coq Using Bisimulation-Up-To Techniques
International Conference on Interactive Theorem Proving, pp. 354-369.
- ^
D. Hausmann, T. Mossakowski, L. Schroder.
Iterative Circular Coinduction for CoCasl in Isabelle/HOL
International Conference on Fundamental Approaches to Software Engineering, pp. 341-356.
- ^
K. Rustan M. Leino, M. Moskal.
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier
International Symposium on Formal Methods, pp. 382-398.
- ^
Formal Systems Laboratory | Circ Prover.
https://fsl.cs.illinois.edu/index.php/Circ
External links
|
---|
International | |
---|
National | |
---|
Academics | |
---|
|
|