Grigore Rosu

For More Information

• Personal webpage
• Formal systems laboratory (research group)
• Runtime Verification, Inc.

Education

• Ph.D. in Computer Science, University of California at San Diego, 2000 Thesis: “Hidden Logic”. Department of Computer Science and Engineering, University of California at San Diego, 4 September 2000.
• M.S. in Fundamentals of Computing, University of Bucharest, Romania, 1996
• B.A. in Mathematics, University of Bucharest, Romania, 1995

Biography

Grigore Rosu does research in design, semantics and implementation of programming and specification languages, automated software engineering and formal methods, especially push-button techniques for certification, monitoring, synthesis and modularization, and in automated reasoning about computer systems, applications of logics, theorem proving, algorithms, (co)algebra, and category theory. He teaches classes on software engineering, programming languages, formal methods, and runtime verification. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000 and his M.S. at the University of Bucharest, Romania, in 1996. Grigore was offered the CAREER award by the NSF in 2005, the outstanding junior award by the CS Department at UIUC in 2005, and the Dean's award for excellence in research by the College of Engineering at UIUC in 2014. He won the ASE IEEE/ACM most influential paper award in 2016 and the RV test of time award for papers published in 2001 that shaped the runtime verification field, and distinguished/best paper awards at ASE 2008, ASE 2016, OOPSLA 2016, ETAPS 2002. He was ranked a UIUC excellent teacher in Spring 2013, Fall 2012, Spring 2008 and Fall 2004.

Rosu is known for work in runtime verification, the K framework, matching logic, and automated coinduction.

Runtime verification was coined by Havelund and Rosu as the name of a workshop they started in 2001, aimed at addressing problems at the boundary between formal verification and testing. Since 2001, runtime verification (RV) has grown into an active and diverse community, with its own international conference. The underlying idea of RV is to verify a system while it executes, where the system is either instrumented or simulated in an environment in which efficient monitors are generated from specifications and checked against the running system. Combined with recovery when properties are violated, RV can be used as a scalable alternative to formal verification, yielding the same correctness guarantees but at a cost fraction. Runtime verification has got significant traction in the formal verification and software engineering communities, where major conferences include special tracks named Runtime Verification. Within the RV field, Rosu and his collaborators introduced several notions, seminal algorithms and techniques for parametric property monitoring, efficient monitor synthesis, runtime predictive analysis, as well as monitoring-oriented programming as a programming paradigm where a formal specification and an implementation form together a (runtime verified) system. In 2010, Rosu founded the company Runtime Verification, Inc. , as a vehicle to productize and commercialize RV technology to customers such as NASA, Boeing, Toyota, Denso, as well as emerging companies in the blockchain space such as Ethereum Foundation, IOHK, Tezos, Algorand, Maker, Gnosis, etc.

The K framework was proposed by Rosu together with his FSL lab in 2003, as an executable semantic framework. Programming languages, type systems and formal analysis tools can be defined uniformly in the K framework, using configurations, computations and rewrite rules. The distinctive feature of K is that once a system is formalized as a K definition, all the tools needed for that system, from concrete execution engines (interpreters, virtual machines (VMs), compilers) to symbolic execution and formal verification tools, can and should be derived automatically or semi-automatically, correct-by-construction. The goal of K is to put an end to the adhoc language tool development. Several complete semantics of real-life programming languages, such as C, Java, JavaScript, Python, and the Ethereum Virtual Machine, have been formally defined in K.

Matching logic is a unifying logic for programming languages, specification, and verification. Matching logic is as expressive as first-order logic (FOL) plus induction, but it provides a compact notation that captures, as syntactic sugar, several logics and formalisms of critical importance such as: algebraic specification and initial algebra semantics, FOL 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, modal μ-calculus, and so on.

Rosu proposed circular coinduction in his PhD thesis, 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 or incorporated in provers such as Coq, Isabelle/HOL, and CIRC.

Other Professional Employment

• President & CEO. Runtime Verification, Inc. 2010 to present.
• Visiting Researcher. Microsoft Research, Redmond, Washington. On sabbatical leave from the University of Illinois. August to December 2008.
• Research Scientist. NASA Ames Research Center, California, USA. Automated Software Engineering Group. Hired by the Research Institute for Advanced Computer Science of the Universities Space Research Association, 2000-2002.

Research Interests

• Software and software related aspects.
• Design, semantics and implementation of programming and specification languages.
• Automated software engineering and formal methods, especially "push-button" techniques for certification, monitoring synthesis and modularization.
• Automated reasoning about computer systems, applications of logics, Theorem proving. Algorithms, (co)algebra, category theory.

Selected Articles in Journals

• G. Rosu and F. Chen, “Semantics and Algorithms for Parametric Monitoring”, Logical Methods in Computer Science, Volume 8, Issue 1, 2012, pages 1-47.

Articles in Conference Proceedings

• C. Hathhorn, C. Ellison and G. Rosu. “Defining the Undefinedness of C”. Proceedings of the 36th ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI’15, Portland, Oregon, 13-17 June 2015. ACM 2015. Acceptance rate 58/303 (19%).
• D. Park, A. Stefanescu, and G. Rosu, “KJS: A Complete Formal Semantics of JavaScript”. Proceedings of the 36th ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI’15, Portland, Oregon, 13-17 June 2015. ACM 2015. Acceptance rate 58/303 (19%).
• J. Huang, Q. Luo, and G. Rosu, “GPredict: Generic Predictive Concurrency Analysis”. Proceedings of the 37th International Conference on Software Engineering, ICSE’11, Florence, Italy, 16-24 May 2015. ACM 2015. Acceptance rate 84/452 (18.5%).
• D. Bogdanas and G. Rosu, "K-Java: A Complete Semantics of Java," Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'15, Mumbai,India, 12-18 January, 2015. ACM, pages 445-456.
• A. Stefanescu, S. Ciobaca, R. Mereuta, B. Moore, T. Serbanuta, and G. Rosu, "All-Path Reachability Logic". Proceedings of the 25th International Conference on Rewriting Techniques and Applications, RTA'14, and 12th International Conference on Typed Lambda Calculus and Applications, TLCA'14, Vienna, Austria, 14-17 July 2014. Lecture Notes in Computer Science, Volume 8560, 2014, pages 425-440. Acceptance rate 31/87 (35.6%).
• J. Huang, P. Meredith and G. Rosu, "Maximal Sound Predictive Race Detection with Control Flow Abstraction", Proceedings of the 35th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'14), Edinburgh, UK, 9-11 June 2014. ACM, to appear. Acceptance rate 52/287 (18.1\%).
• Q. Luo and G. Rosu, "EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs", Proceedings of the International Symposium in Software Testing and Analysis (ISSTA'13), Lugano, Switzerland, 15-20 July 2013. ACM, pages 156-166. Acceptance rate 32/124 (25.8\%)
• G. Rosu and A. Stefanescu, "Reachability Logic", Proceedings of the 28th Annual ACM/IEEE Symposium of Logic in Computer Science (LICS'13), New Orleans, USA, 25-27 June 2013, ACM/IEEE, . Acceptance rate 57/165 (34.5%).
• G. Rosu and A. Stefanescu, "Checking reachability using matching logic," Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA'12), part of SPLASH 2012, Tucson, AZ, USA, 21-25 October 2012. ACM, pages 555-574, 2012. Acceptance rate 57/228 (25%).

Research Honors

• Test of time award (for paper published in RV 2001) (2018)
• Distinguished paper award at ASE'16 (2016)
• Most influential paper award (for paper published in ASE 2001) (2016)
• Ad Astra (excellence in mathematics and computer science research) (2016)
• Distinguished paper award at OOPSLA'16 (2016)
• Dean's Award for Excellence in Research (2014)
• Distinguished paper award at ASE'08 (2008)
• C.W. Gear Outstanding Junior Faculty Award (2005)
• NSF CAREER Award, under "Software Engineering and Languages" (2005)
• Best software science paper at ETAPS'02 (2002)
• Irina Gorun-Bercovici memorial prize (1997)