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)
  • Eckhardt, Jonas; Muelbauer, Tobias; Meseguer, Jose (2011-09-27)
    Many formal languages use the concept of names to range over essential entities of the language and are usually equipped with special binding constructs for names. For example, the lambda-calculus uses variables as ...

    application/pdf

    application/pdfPDF (357Kb)
  • 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)
  • Meseguer, Jose; Skeirik, Stephen (2015-06-13)
    A pattern, i.e., a term possibly with variables, denotes the set (language) of all its ground instances. In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on languages. ...

    application/pdf

    application/pdfPDF (482Kb)
  • 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)