Grigore Roșu (born December 12, 1971) is a

computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

professor Professor (commonly abbreviated as Prof.) is an Academy, academic rank at university, universities and other tertiary education, post-secondary education and research institutions in most countries. Literally, ''professor'' derives from Latin ...

at the

University of Illinois at Urbana-Champaign The University of Illinois Urbana-Champaign (UIUC, U of I, Illinois, or University of Illinois) is a public land-grant research university in the Champaign–Urbana metropolitan area, Illinois, United States. Established in 1867, it is the f ...

and a

researcher Research is creative and systematic work undertaken to increase the stock of knowledge. It involves the collection, organization, and analysis of evidence to increase understanding of a topic, characterized by a particular attentiveness to ...

in the Information Trust Institute.Grigore Rosu'

/ref> He is known for his contributions in runtime verification, Runtime Verification, the K framework, K framework. https://kframework.org matching logic, Matching logic. https://matching-logic.org automated

coinduction In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects. Coinduction is the mathematical dual to structural induction. Coinductively defined data types are known as coda ...

. Automated coinduction. https://fsl.cs.illinois.edu/index.php/Circ , and for foundin
Runtime Verification, Inc.
and
Pi Squared, Inc.

Biography

Roșu received a

B.A. A Bachelor of Arts (abbreviated B.A., BA, A.B. or AB; from the Latin ', ', or ') is the holder of a bachelor's degree awarded for an undergraduate program in the liberal arts, or, in some cases, other disciplines. A Bachelor of Arts degree ...

Mathematics Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...

in 1995 and an

M.S. A Master of Science (; abbreviated MS, M.S., MSc, M.Sc., SM, S.M., ScM or Sc.M.) is a master's degree. In contrast to the Master of Arts degree, the Master of Science degree is typically granted for studies in sciences, engineering and medicine ...

in Fundamentals of Computing in 1996, both from the

University of Bucharest The University of Bucharest (UB) () is a public university, public research university in Bucharest, Romania. It was founded in its current form on by a decree of Prince Alexandru Ioan Cuza to convert the former Princely Academy of Bucharest, P ...

, Romania, and a Ph.D. in

Computer Science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

in 2000 from the

University of California at San Diego The University of California, San Diego (UC San Diego in communications material, formerly and colloquially UCSD) is a public land-grant research university in San Diego, California, United States. Established in 1960 near the pre-existing Sc ...

. After completing his doctorate, he joined

NASA The National Aeronautics and Space Administration (NASA ) is an independent agencies of the United States government, independent agency of the federal government of the United States, US federal government responsible for the United States ...

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 The University of Illinois Urbana-Champaign (UIUC, U of I, Illinois, or University of Illinois) is a public land-grant research university in the Champaign–Urbana metropolitan area, Illinois, United States. Established in 1867, it is the f ...

as an

assistant professor Assistant professor is an academic rank just below the rank of an associate professor used in universities or colleges, mainly in the United States, Canada, Japan, and South Korea. Overview This position is generally taken after earning a doct ...

, later becoming an

associate professor Associate professor is an academic title with two principal meanings: in the North American system and that of the ''Commonwealth system''. In the ''North American system'', used in the United States and many other countries, it is a position ...

in 2008 and a

full professor Professor (commonly abbreviated as Prof.) is an academic rank at universities and other post-secondary education and research institutions in most countries. Literally, ''professor'' derives from Latin as a 'person who professes'. Professors ...

in 2014. In 2003, Roșu, alongside his studen
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 The Boeing Company, or simply Boeing (), is an American multinational corporation that designs, manufactures, and sells airplanes, rotorcraft, rockets, satellites, and missiles worldwide. The company also provides leasing and product support s ...

and

Toyota is a Japanese Multinational corporation, multinational Automotive industry, automotive manufacturer headquartered in Toyota City, Aichi, Japan. It was founded by Kiichiro Toyoda and incorporated on August 28, 1937. Toyota is the List of manuf ...

in the embedded systems domain. In late 2023, he founde
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 (for an ASE 2001 paper) * Runtime Verification (RV) Test of Time awards in 2018 (for an RV 2001 paper) and in 2023 (for an RV 2003 paper) * ACM distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016 * Best software science paper award at ETAPS 2002 *

NSF CAREER award The National Science Foundation CAREER award is the most prestigious award presented by the National Science Foundation (NSF) of the United States Federal Government to support junior faculty who exemplify the role of teacher-scholars through rese ...

in 2005 * Ad AStra award in 2016 * Fellow of the Institute of Electrical and Electronics Engineers (IEEE) * Fellow of the American Association for the Advancement of Science (AAAS)

Contributions

Roșu coined the term " runtime verification, Runtime Verification" together with Havelund as the name of a workshop International Conference of Runtime Verification. https://runtime-verification.org started in 2001, aiming at addressing problems at the boundary between

formal verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal ver ...

and testing. Roșu and his collaborators introduced algorithms and techniques for parametric property monitoring, efficient monitor synthesis, runtime predictive analysis, and monitoring-oriented programming. Monitoring-Oriented Programming. https://fsl.cs.illinois.edu/index.php/Monitoring-Oriented_Programming Roșu created and led the design and development of the K framework, which is an executable

semantic Semantics is the study of linguistic Meaning (philosophy), meaning. It examines what meaning is, how words get their meaning, and how the meaning of a complex expression depends on its parts. Part of this process involves the distinction betwee ...

framework where

programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...

type system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...

s, and

formal analysis In art history, formalism is the study of art by analyzing and comparing form and Style (visual arts), style. Its discussion also includes the way objects are made and their purely visual or material aspects. In painting, formalism emphasizes compo ...

tools are defined using configurations,

computation A computation is any type of arithmetic or non-arithmetic calculation that is well-defined. Common examples of computation are mathematical equation solving and the execution of computer algorithms. Mechanical or electronic devices (or, hist ...

s, and

rewrite rule In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a well-formed formula, formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewr ...

s. Language tools such as

interpreter Interpreting is translation from a spoken or signed language into another language, usually in real time to facilitate live communication. It is distinguished from the translation of a written text, which can be more deliberative and make use o ...

virtual machine In computing, a virtual machine (VM) is the virtualization or emulator, emulation of a computer system. Virtual machines are based on computer architectures and provide the functionality of a physical computer. Their implementations may involve ...

compiler In computing, a compiler is a computer program that Translator (computing), translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primaril ...

symbolic execution In computer science, symbolic execution (also symbolic evaluation or symbex) is a means of analyzing a program to determine what inputs cause each part of a program to execute. An interpreter follows the program, assuming symbolic values for i ...

and

tools, are automatically or semi-automatically generated by the K framework. Formal semantics of several known programming languages, such as C,

Java Java is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea (a part of Pacific Ocean) to the north. With a population of 156.9 million people (including Madura) in mid 2024, proje ...

JavaScript JavaScript (), often abbreviated as JS, is a programming language and core technology of the World Wide Web, alongside HTML and CSS. Ninety-nine percent of websites use JavaScript on the client side for webpage behavior. Web browsers have ...

Python Python may refer to: Snakes * Pythonidae, a family of nonvenomous snakes found in Africa, Asia, and Australia ** ''Python'' (genus), a genus of Pythonidae found in Africa and Asia * Python (mythology), a mythical serpent Computing * Python (prog ...

, and Ethereum Virtual Machine are defined using the K framework. Roșu introduced matching logic as a foundation for the K framework and for

specification A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard. There are different types of technical or engineering specificati ...

, and verification. It is as expressive as

first-order logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...

plus

mathematical induction Mathematical induction is a method for mathematical proof, proving that a statement P(n) is true for every natural number n, that is, that the infinitely many cases P(0), P(1), P(2), P(3), \dots all hold. This is done by first proving a ...

, and uses a compact notation to capture, as syntactic sugar, several

formal system A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms. In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in ma ...

s of critical importance, such as

algebraic specification Algebraic specification is a software engineering technique for formally specifying system behavior. It was a very active subject of computer science research around 1980. Overview Algebraic specification seeks to systematically develop more effic ...

and

initial algebra In mathematics, an initial algebra is an initial object in the Category (mathematics), category of F-algebra, -algebras for a given endofunctor . This initiality provides a general framework for mathematical induction, induction and recursion. ...

semantics,

with

least fixed point In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set ("poset" for short) to itself is the fixed point which is less than each other fixed po ...

s, typed or untyped lambda-calculi, dependent type systems, separation logic with recursive predicates, rewriting logic,

Hoare logic Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and l ...

temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...

s, dynamic logic, and the

modal μ-calculus In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point opera ...

. Roșu's Ph.D. thesis proposed circular coinduction 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

, and has been implemented in

Coq Coenzyme Q10 (CoQ10 ), also known as ubiquinone, is a naturally occurring biochemical cofactor (coenzyme) and an antioxidant produced by the human body. It can also be obtained from dietary sources, such as meat, fish, seed oils, vegetables, ...

, Isabelle/HOL,

Dafny Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go, and Python. It supports formal specification through preconditions, postconditions, loop invariants, loo ...

, and as part of the CIRC theorem prover. Formal Systems Laboratory , Circ Prover. https://fsl.cs.illinois.edu/index.php/Circ

References

External links

Home pageLinkedIn
* Publications
Google
{{DEFAULTSORT:Rosu, Grigore American computer scientists 1971 births University of Bucharest alumni University of Illinois Urbana-Champaign faculty Living people Formal methods people Romanian emigrants to the United States