Browse Research and Tech Reports - Computer Science by Author "Ellison, Chucky M."

  • Ellison, Chucky M.; Rosu, Grigore (2012-04-27)
    This paper investigates undefined behavior in C and offers a few simple techniques for operationally specifying such behavior formally. A semantics-based undefinedness checker for C is developed using these techniques, as ...

    application/pdf

    application/pdfPDF (257kB)
  • Ellison, Chucky M.; Rosu, Grigore (2011-07-17)
    This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 770 of 776 test programs. It is the most ...

    application/pdf

    application/pdfPDF (701kB)
  • Ellison, Chucky M.; Rosu, Grigore (2011-11-22)
    This paper describes an executable formal semantics of C expressed using a formalism based on term rewriting. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully ...

    application/pdf

    application/pdfPDF (591kB)
  • Rosu, Grigore; Ellison, Chucky M.; Schulte, Wolfram (2009-07-25)
    Rewriting logic semantics (RLS) is a definitional framework in which a programming language is defined as a rewrite theory: the algebraic signature defines the program configurations, the equations define structural ...

    application/pdf

    application/pdfPDF (395kB)
  • 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)
  • 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)