Browse by Author "Meseguer, Jose"

  • Boronat, Artur; Meseguer, Jose (2007-10)
    Model-Driven Development is a field in Software Engineering that, for several years, has represented software artifacts as models in order to improve productivity, quality, and cost effectiveness. Models provide a more ...

    application/pdf

    application/pdfPDF (3Mb)
  • Boronat, Artur; Meseguer, Jose (2008-08)
    In the denition of domain-specic languages a MOF metamodel is used to dene the main types of its abstract syntax, and OCL invariants are used to add semantic constraints. The semantics of a metamodel denition can be given ...

    application/pdf

    application/pdfPDF (372Kb)
  • Boronat, Artur; Meseguer, Jose (2008-08)
    In the denition of domain-specic languages a MOF metamodel is used to dene the main types of its abstract syntax, and OCL invariants are used to add semantic constraints. The semantics of a metamodel denition can be given ...

    application/pdf

    application/pdfPDF (372Kb)
  • Garrido, Alejandra; Meseguer, Jose; Johnson, Ralph (2006-02)
    Refactoring has become a popular technique for the development and maintenance of object-oriented systems. We have been working on the refactoring of C programs, including the C preprocessor (Cpp), and we have built ...

    application/pdf

    application/pdfPDF (201Kb)
  • Meseguer, Jose; Palomino, Miguel; Marti-Oliet, Narciso (2007-08)
    A fruitful approach to the study of state-based systems consists in their mathematical formalization by means of models like Kripke structures. They allow verification of their associated properties using simulations that ...

    application/pdf

    application/pdfPDF (490Kb)
  • Cholewa, Andrew; Escobar, Santiago; Meseguer, Jose (2014-08-29)
    For an unconditional equational theory (Σ,E) whose oriented equations E⃗ are confluent and terminating, narrowing provides an E-unification algorithm. This has been generalized by various authors in two directions: (i) by ...

    application/pdf

    application/pdfPDF (589Kb)
  • Escobar, Santiago; Meseguer, Jose; Sasse, Ralf (2008-04)
    An equational theory decomposed into a set B of equational axioms and a set \Delta of rewrite rules has the \emph{finite variant} (FV) \emph{property} in the sense of Comon-Lundh and Delaune iff for each term t there is a ...

    application/pdf

    application/pdfPDF (468Kb)
  • Rocha, Camilo; Meseguer, Jose (2007-02)
    We present four equational theories that are isomorphic to the traditional Boolean theory and show that each one of them gives rise to a canonical rewrite system modulo associativity, thus providing four decision procedures ...

    application/pdf

    application/pdfPDF (658Kb)
  • Meredith, Patrick; Katelman, Michael; Meseguer, Jose; Roşu, Grigore (2010-07)
    This paper describes a formal executable semantics for the Verilog hardware description language. The goal of our formalization is to provide a concise and mathematically rigorous reference augmenting the prose of ...

    application/pdf

    application/pdfPDF (279Kb)
  • Garrido, Alejandra; Meseguer, Jose (2006-05)
    There is an extensive literature about refactorings of object-oriented programs, and many refactoring tools for the Java programming language. However, except for a few studies, in practice it is difficult to find precise ...

    application/pdf

    application/pdfPDF (172Kb)
  • Sasse, Ralf; Meseguer, Jose (2006-02)
    Java+ITP is an experimental tool for the verification of properties of a sequential imperative subset of the Java language. It is based on an algebraic continuation passing style (CPS) semantics of this fragment as an ...

    application/pdf

    application/pdfPDF (264Kb)
  • Hendrix, Joe; Meseguer, Jose (2007-02)
    We propose three different notions of completeness for term rewrite specifications supporting order-sorted signatures, deduction modulo axioms, and context-sensitive rewriting relative to a replacement map mu. Our three ...

    application/pdf

    application/pdfPDF (439Kb)
  • Sha, Lui; Al-Nayeem, Abdullah; Sun, Mu; Meseguer, Jose; Olveczky, Peter C. (2009-05-26)
    In networked cyber physical systems real time global computations, e.g., the supervisory control of a ight control system, require consistent views, consistent actions and synchronized state transitions across net- work ...

    application/pdf

    application/pdfPDF (376Kb)
  • Farzan, Azadeh; Meseguer, Jose (2005-06)
    Partial order reduction (POR) capabilities are typically added by extending a model checking algorithm supporting analysis of programs in a given programming language. In this paper we propose a generic method to generate ...

    application/pdf

    application/pdfPDF (189Kb)
  • Agha, Gul A.; Meseguer, Jose; Sen, Koushik (2005-03)
    We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level ...

    application/pdf

    application/pdfPDF (228Kb)
  • Rocha, Camilo; Meseguer, Jose (2007-12)
    We present an equational decision procedure a la Dijkstra & Scholten for the `Syllogistic Logic with Complements'. First, we give an equational axiomatization of Dijkstra & Scholten's propositional logic and show how it ...

    application/pdf

    application/pdfPDF (333Kb)
  • 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)
  • AlTurki, Musab; Meseguer, Jose (2007-11)
    Orc is a language for \emph{orchestration} of web services developed by J. Misra that offers simple, yet powerful and elegant, constructs to succinctly program sophisticated web orchestration applications. However, because ...

    application/pdf

    application/pdfPDF (757Kb)
  • 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)
  • Katelman, Michael; Keller, Sean; Meseguer, Jose (2010-02-03)
    We give source code for an executable formal semantics of production rule sets (PRS) in Maude, along with several example circuits that can be model checked for hazard-free and deadlock-free operation using our semantics ...

    application/octet-stream

    application/octet-streamUnknown (26Kb)