Browse by Author "Rosu, Grigore"

  • 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 (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 (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-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; 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; Meseguer, Jose (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)
  • 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)
  • 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)
  • Meseguer, Jose; Rosu, Grigore (2005-09)
    Rewriting logic is a flexible and expressive logical framework that unifies denotational semantics and SOS in a novel way, avoiding their respective limitations and allowing very succinct semantic definitions. The fact ...

    application/pdf

    application/pdfPDF (807Kb)
  • Rosu, Grigore; Schulte, Wolfram; Serbanuta, Traian Florin (2009-03)
    C is the most widely used imperative system's implementation language. While C provides types and high-level abstractions, its design goal has been to provide highest performance which often requires low-level access to ...

    application/pdf

    application/pdfPDF (286Kb)
  • Rosu, Grigore; Schulte, Wolfram; Serbanuta, Traian Florin (2009-03)
    C is the most widely used imperative system's implementation language. While C provides types and high-level abstractions, its design goal has been to provide highest performance which often requires low-level access to ...

    application/pdf

    application/pdfPDF (286Kb)
  • Jin, Dongyun; Meredith, Patrick O'Neil; Rosu, Grigore (2012-04-24)
    Runtime monitoring is an effective means to improve the reliability of systems. In recent years, parametric monitoring, which is highly suitable for object-oriented systems, has gained significant traction. Previous ...

    application/pdf

    application/pdfPDF (275Kb)
  • Popescu, Andrei; Serbanuta, Traian Florin; Rosu, Grigore (2005-05)
    Interpolation results are investigated for various types of formulae. By shifting the focus from syntactic to semantic interpolation, we generate, prove and classify more than twenty interpolation results for first-order ...

    application/pdf

    application/pdfPDF (309Kb)