Browse by Author "Rosu, Grigore"

  • Ilseman, Michael; Ellison, Chucky M.; Rosu, Grigore (2010-12-14)
    This paper describes a completely automated method for generating efficient and competitive interpreters from formal semantics expressed in Rewriting Logic. The semantics are compiled into OCaml code, which then acts as ...

    application/pdf

    application/pdfPDF (257Kb)
  • application/pdf

    application/pdfPDF (264Kb)
  • Rosu, Grigore (2007-02)
    Various definitions of safety properties as sets of execution traces have been introduced in the literature, some over finite traces, others over infinite traces, yet others over both finite and infinite traces. By employing ...

    application/pdf

    application/pdfPDF (388Kb)
  • Rosu, Grigore (2010-02-05)
    K is an executable semantic framework in which programming languages, calculi, as well as type systems or formal analysis tools can be defined making use of configurations, computations and rules. Configurations organize ...

    application/pdf

    application/pdfPDF (748Kb)
  • Chen, Feng; Rosu, Grigore (2007-01)
    Happen-before causal partial order relations have been widely used in concurrent program verification and testing. In this paper, we present a parametric approach to happen-before causal partial orders. All existing variants ...

    application/pdf

    application/pdfPDF (130Kb)
  • Chen, Feng; Rosu, Grigore (2006-04)
    A parametric approach to control dependence is presented, where the parameter is any prefix-invariant property on paths in the control-flow graph. Existing control dependencies, both direct and indirect, can be obtained ...

    application/pdf

    application/pdfPDF (156Kb)
  • Rosu, Grigore; Chen, Feng (2008-07)
    Trace analysis plays a fundamental role in many program analysis approaches, such as runtime verification, testing, monitoring, and specification mining. Recent research efforts bring empirical evidence that execution ...

    application/pdf

    application/pdfPDF (649Kb)
  • Hills, Mark; Chen, Feng; Rosu, Grigore (2008-01)
    Many programs make implicit assumptions about data. Common assumptions include whether a variable has been initialized or can only contain non-null references. Domain-specific examples are also common, with many scientific ...

    application/pdf

    application/pdfPDF (270Kb)
  • Chen, Feng; Rosu, Grigore (2006-04)
    A runtime analysis technique is presented, which can predict concurrency errors in multithreaded systems by observing potentially non-erroneous executions. It builds upon a novel causal partial order, sliced causality, ...

    application/pdf

    application/pdfPDF (157Kb)
  • Chen, Feng; Rosu, Grigore (2005-11)
    A runtime analysis technique is presented, which can predict errors in multi-threaded systems by examining event traces generated by executions of these systems even when they are successful. The technique is based on a ...

    application/pdf

    application/pdfPDF (268Kb)
  • Chen, Feng; Rosu, Grigore (2005-07)
    We present a technique to predict property violations in multi-threaded programs from successful executions. An appealing aspect of our technique is that it is entirely automatic; another is that no special simulation or ...

    application/pdf

    application/pdfPDF (365Kb)
  • Rosu, Grigore; Moore, Brandon (unpublished, 2015-02-08)
    We present a program verification framework based on coinduction, which makes it feasible to verify programs directly against an operational semantics, without requiring intermediates like axiomatic semantics or ...

    application/pdf

    application/pdfPDF (252Kb)
  • Rosu, Grigore; Stefanescu, Andrei; Ciobaca, Stefan; Moore, Brandon (2012-07)
    Abstract. This paper introduces *reachability logic*, a language-independent seven-rule proof system for deriving reachability properties of systems. The key ingredients of *reachability logic* are its sentences, which are ...

    application/pdf

    application/pdfPDF (358Kb)
  • Stefanescu, Andrei; Ciobaca, Stefan; Moore, Brandon; Serbanuta, Traian Florin; Rosu, Grigore (2013-11)
    This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (concurrent) languages, referred to as reachability logic. The proof system derives partial-correctness ...

    application/pdf

    application/pdfPDF (237Kb)
  • Hills, Mark; Serbanuta, Traian Florin; Rosu, Grigore (2005-12)
    A rewrite logic semantic definitional framework for programming languages is introduced, called K, together with partially automated translations of K language definitions into rewriting logic and into C. The framework is ...

    application/pdf

    application/pdfPDF (209Kb)
  • Chen, Feng; Hills, Mark; Rosu, Grigore (2006-03)
    This paper introduces a framework for rapid prototyping of object oriented programming languages and corresponding analysis tools. It is based on formal definitions of language features in rewrite logic, a simple and ...

    application/pdf

    application/pdfPDF (257Kb)
  • Hills, Mark; Rosu, Grigore (2006-10)
    This paper introduces a framework for the rapid prototyping of object oriented programming languages. This framework is based on specifying the semantics of a language using term rewriting and a continuation-based ...

    application/pdf

    application/pdfPDF (244Kb)
  • Serbanuta, Traian Florin; Rosu, Grigore (2006-10)
    We show how one can use rewriting logic to faithfully capture (not implement) various operational semantic frameworks as rewrite logic theories, namely big-step and small-step semantics, reduction semantics using evaluation ...

    application/pdf

    application/pdfPDF (374Kb)
  • Serbanuta, Traian Florin; Rosu, Grigore; Meseguer, Jos�� (2007-02)
    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 ...

    application/pdf

    application/pdfPDF (430Kb)
  • Ellison, Chucky M.; Serbanuta, Traian Florin; Rosu, Grigore (2008-03)
    Meseguer and Rosu proposed rewriting logic semantics (RLS) as a programming language definitional framework that unifies operational and algebraic denotational semantics. Once a language is defined as an RLS theory, many ...

    application/pdf

    application/pdfPDF (383Kb)