Author name cluster

Grigore Roşu

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

1 author row

TCS Journal 2026 Journal Article

A unifying logical foundation for initial algebra semantics and induction

Xiaohong Chen
Dorel Lucanu
Grigore Roşu

Initial algebra semantics provides a generic and principled framework to study induction. In this paper, we give a complete formalization of ini- tial algebra semantics and inductive reasoning using matching logic—a small and unifying logic for formal semantics of programming languages. Specifi- cally, we define initial algebra semantics as matching logic theories and derive induction/iteration/primitive-recursion principles as formal theorems within matching logic, using its proof system. This way, we obtain, for the first time, a rigorous logical foundation for general initial algebra semantics and induc- tion, both proof-theoretically and model-theoretically. As a bonus, matching logic admits the smallest known proof checker for a logic supporting inductive proofs, of only 240 lines of code.

Details DOI

TCS Journal 2015 Journal Article

Term-generic logic

Andrei Popescu
Grigore Roşu

We introduce term-generic logic (TGL), a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring terms to only provide free variable and substitution operators satisfying some reasonable axioms. TGL has a notion of model that generalizes both first-order models and Henkin models of the λ-calculus. The abstract notions of term syntax and model are shown to be sufficient for obtaining the completeness theorem of a Gentzen system generalizing that of first-order logic. Various systems featuring bindings and contextual reasoning, ranging from pure type systems to the π-calculus, are captured as theories inside TGL. For two particular, but rather typical instances—untyped λ-calculus and System F—the general-purpose TGL models are shown to be equivalent with standard ad hoc models.

Details DOI

I&C Journal 2013 Journal Article

The rewriting logic semantics project: A progress report

José Meseguer
Grigore Roşu

Rewriting logic is an executable logical framework well suited for the semantic definition of languages. Any such framework has to be judged by its effectiveness to bridge the existing gap between language definitions on the one hand, and language implementations and language analysis tools on the other. We give a progress report on how researchers in the rewriting logic semantics project are narrowing the gap between theory and practice in areas such as: modular semantic definitions of languages; scalability to real languages; support for real time; semantics of software and hardware modeling languages; and semantics-based analysis tools such as static analyzers, model checkers, and program provers.

Details DOI

I&C Journal 2009 Journal Article

A rewriting logic approach to operational semantics

Traian Florin Şerbănuţă
Grigore Roşu
José Meseguer

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.

Details DOI

TCS Journal 2009 Journal Article

A semantic approach to interpolation

Andrei Popescu
Traian Florin Şerbănuţă
Grigore Roşu

Craig interpolation is investigated for various types of formulae. By shifting the focus from syntactic to semantic interpolation, we generate, prove and classify a series of interpolation results for first-order logic. A few of these results non-trivially generalize known interpolation results; all the others are new. We also discuss some applications of our results to the theory of institutions and of algebraic specifications, and a Craig–Robinson version of these results.

Details DOI

TCS Journal 2007 Journal Article

The rewriting logic semantics project

José Meseguer
Grigore Roşu

Rewriting logic is a flexible and expressive logical framework that unifies algebraic denotational semantics and structural operational semantics (SOS) in a novel way, avoiding their respective limitations and allowing succinct semantic definitions. The fact that a rewrite logic theory’s axioms include both equations and rewrite rules provides a useful “abstraction dial” to find the right balance between abstraction and computational observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.

Details DOI

TCS Journal 2005 Journal Article

Combining test case generation and runtime verification

Cyrille Artho
Howard Barringer
Allen Goldberg
Klaus Havelund
Sarfraz Khurshid
Mike Lowry
Corina Pasareanu
Grigore Roşu

Software testing is typically an ad hoc process where human testers manually write test inputs and descriptions of expected test results, perhaps automating their execution in a regression suite. This process is cumbersome and costly. This paper reports results on a framework to further automate this process. The framework consists of combining automated test case generation based on systematically exploring the input domain of the program with runtime verification, where execution traces are monitored and verified against properties expressed in temporal logic. Capabilities also exist for analyzing traces for concurrency errors, such as deadlocks and data races. The input domain of the program is explored using a model checker extended with symbolic execution. Properties are formulated in an expressive temporal logic. A methodology is advocated that automatically generates properties specific to each input rather than formulating properties uniformly true for all inputs. The paper describes an application of the technology to a NASA rover controller.

Details DOI

TCS Journal 2004 Journal Article

Behavioral abstraction is hiding information

Grigore Roşu

We show that for any behavioral Σ -specification B there is an ordinary algebraic specification B ˜ over a larger signature, such that a model behaviorally satisfies B iff it satisfies, in the ordinary sense, the Σ -theorems of B ˜. The idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. We develop a procedure, called unhiding, which takes a finite B and produces a finite B ˜. The practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.

Details DOI

TCS Journal 2001 Journal Article

Equational axiomatizability for coalgebra

Grigore Roşu

A characterization result for equationally definable classes of certain coalgebras (including basic hidden algebra) shows that a class of coalgebras is definable by equations if and only if it is closed under coproducts, quotients, sources of morphisms and representative inclusions. The notions of equation and satisfaction are axiomatized in order to include the different approaches in the literature.

Details DOI