Submitted Successfully!
To reward your contribution, here is a gift for you: A free trial for our video production service.
Thank you for your contribution! You can also upload a video entry or images related to this topic.
Version Summary Created by Modification Content Size Created at Operation
1 handwiki
Amina Yu
 -- 497 2022-12-05 01:54:17 |
2 update layout
Amina Yu
 Meta information modification 518 2022-12-05 02:28:52 | |
3 update layout
Amina Yu
 Meta information modification 518 2022-12-06 08:12:01 |

Video Upload Options

We provide professional Video Production Services to translate complex research into visually appealing presentations. Would you like to try it?
No, upload directly Yes

Confirm

Are you sure to Delete?
Yes No
Cite
If you have any further questions, please contact Encyclopedia Editorial Office.
HandWiki. Grigore Rosu. Encyclopedia. Available online: https://encyclopedia.pub/entry/37920 (accessed on 18 November 2024).
HandWiki. Grigore Rosu. Encyclopedia. Available at: https://encyclopedia.pub/entry/37920. Accessed November 18, 2024.
HandWiki. "Grigore Rosu" Encyclopedia, https://encyclopedia.pub/entry/37920 (accessed November 18, 2024).
HandWiki. (2022, December 05). Grigore Rosu. In Encyclopedia. https://encyclopedia.pub/entry/37920
HandWiki. "Grigore Rosu." Encyclopedia. Web. 05 December, 2022.
Grigore Rosu
Edit
The content is sourced from: https://handwiki.org/wiki/Biography:Grigore_Rosu
computer science coinduction

1. Introduction

Grigore Roșu 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, K framework,[2] matching logic,[3] and automated coinduction.[4]

2. Biography

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

3. Awards

  • IEEE/ACM most influential paper of Automate Software Engineering (ASE) award in 2016[5] (for an ASE 2001 paper[6])
  • Runtime Verification (RV) test of time award[7] (for an RV 2001 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]

4. Contributions

Rosu 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. Rosu 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] Rosu has also founded Runtime Verification, Inc., a company aimed at commercializing runtime verification technology.[19]

Rosu 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.

Rosu 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 modal μ-calculus.

Rosu'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]

Further Reading
In this part, we encourage you to list the link of papers wrote by the character, or published reviews/articles about his/her academic contributions. Edit

References

  1. Grigore Rosu's curriculum vitae http://fsl.cs.illinois.edu/index.php/Grigore_Rosu_-_Curriculum_Vitae
  2. K framework. http://www.kframework.org
  3. Matching logic. http://www.matching-logic.org
  4. Automated coinduction. http://fsl.cs.illinois.edu/index.php/Circ
  5. Most influential papers of Automated Software Engineering. http://ase-conferences.org/Mip.html
  6. K. Havelund, G. Rosu. 2001, Monitoring Programs Using Rewriting, Automated Software Engineering (ASE), pp. 135-143. https://ieeexplore.ieee.org/document/989799
  7. Runtime Verification. https://www.runtime-verification.org/
  8. K. Havelund, G. Rosu. 2001, Monitoring Java Programs with Java PathExplorer, Electronic Notes in Theoretical Computer Science vol. 55(2), pp. 200-217. https://www.sciencedirect.com/science/article/pii/S1571066104002531
  9. ACM SIGSOFT distinguished paper awards. https://www.sigsoft.org/awards/distinguishedPaperAward.html
  10. European Association for the Study of Science and Technology. http://easst.aulp.co.uk/awards-to-date
  11. NSF Award Search: Award#0448501 - CAREER: Runtime Verification and Monitoring. https://www.nsf.gov/awardsearch/showAward?AWD_ID=0448501
  12. Grigore Roșu | Premiile Ad Astra. http://premii.ad-astra.ro/?p=314
  13. Klaus Havelund homepage. https://www.havelund.com/
  14. International Conference of Runtime Verification. http://runtime-verification.org
  15. G. Rosu, F. Chen. 2012, Semantics and Algorithms for Parametric Monitoring Logical Methods in Computer Science (LMCS), vol. 8(1), pp. 1–47. https://lmcs.episciences.org/710/
  16. 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. https://link.springer.com/article/10.1007/s10515-010-0063-y
  17. F. Chen, T. Serbanuta, G. Rosu. 2008, jPredictor: A Predictive Runtime Analysis Tool for Java International Conference on Software Engineering (ICSE), pp. 221–230. https://dl.acm.org/doi/10.1145/1368088.1368119
  18. Monitoring-Oriented Programming. http://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming
  19. Runtimve Verification Inc. https://runtimeverification.com/team/
  20. C. Hathhorn, C. Ellison, G. Rosu. 2015, Defining the Undefinedness of C In Proceedings of Programming Language Design and Implementation (PLDI), pp. 336-345. https://dl.acm.org/citation.cfm?id=2737979
  21. D. Bogdanas, G. Rosu. 2015, K-Java: A Complete Semantics of Java In Proceedings of Principles of Programming Languages (POPL), pp. 445-456. https://dl.acm.org/citation.cfm?id=2676982
  22. 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. https://dl.acm.org/citation.cfm?id=2737991
  23. D. Guth. 2013, M.S. thesis, A Formal Semantics of Python 3.3 University of Illinois at Urbana-Champaign. https://www.ideals.illinois.edu/handle/2142/45275
  24. 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. https://ieeexplore.ieee.org/document/8429306
  25. Y. Gurevich, S. Shelah. 1985, Fixed-point extensions of first-order logic In Proceedings of Foundations of Computer Science (SFCS), pp. 346-353. https://ieeexplore.ieee.org/document/4568160
  26. J. Meseguer. 2012, Twenty Years of Rewriting Logic In the Journal of Logic and Algebraic Programming (JLAP), vol. 81(7-8), pp. 721-781. https://www.sciencedirect.com/science/article/pii/S1567832612000707
  27. Rewriting Logics and Systems, http://www.csl.sri.com/programs/rewriting/
  28. G. Rosu. 2000, Ph.D. thesis Hidden Logic University of California San Diego. http://roger.ucsd.edu/record=b4170032
  29. G. Rosu, D. Lucanu. 2009, Circular Coinduction: A Proof Theoretical Foundation In Proceedings of Algebra and Coalgebra in Computer Science (CALCO), pp. 127-144. https://link.springer.com/chapter/10.1007/978-3-642-03741-2_10
  30. J. Endrullis, D. Hendriks, M. Bodin. Circular Coinduction in Coq Using Bisimulation-Up-To Techniques International Conference on Interactive Theorem Proving, pp. 354-369. https://link.springer.com/chapter/10.1007/978-3-642-39634-2_26
  31. 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. https://link.springer.com/chapter/10.1007/978-3-540-31984-9_26
  32. 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. https://link.springer.com/chapter/10.1007/978-3-319-06410-9_27
  33. Formal Systems Laboratory | Circ Prover. http://fsl.cs.illinois.edu/index.php/Circ
More
©Text is available under the terms and conditions of the Creative Commons-Attribution ShareAlike (CC BY-SA) license; additional terms may apply. By using this site, you agree to the Terms and Conditions and Privacy Policy.
Grigore Rosu
Name: Grigore Rosu
Born: Dec 1971
Birth
Location: Unknown
Title: Professor of computer science
Affiliations: 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
Honor: Unknown
Upload a video for this entry
Information
Subjects: Others
Contributor MDPI registered users' name will be linked to their SciProfiles pages. To register with us, please refer to https://encyclopedia.pub/register :
HandWiki
View Times: 670
Entry Collection: HandWiki
Revisions: 3 times (View History)
Update Date: 06 Dec 2022
Table of Contents
    1000/1000
    Hot Most Recent
    ScholarVision Creations
    Feedback