Browse by Author "Meseguer, Jose"

  • 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)
  • Meseguer, Jose; Sharykin, Raman (2005-10)
    In practice, many stochastic hybrid systems are not autonomous: they are objects that communicate with other objects by exchanging messages through an asynchronous medium such as a network. Issues such as: how to compositionally ...

    application/pdf

    application/pdfPDF (315Kb)
  • Olveczky, Peter C.; Meseguer, Jose; Talcott, Carolyn L. (2004-08)
    This paper describes the application of the Real-Time Maude tool and the Maude formal methodology to the specification and analysis of the AER/NCA suite of active network multicast protocol components. Because of the ...

    application/pdf

    application/pdfPDF (631Kb)
  • Katelman, Michael; Meseguer, Jose (2009-06-03)
    The development of modern ICs requires a huge investment in RTL verification. This is a reflection of brisk release schedules and the complexity of contemporary chip designs. A major bottleneck to reaching verification ...

    application/pdf

    application/pdfPDF (229Kb)
  • Meseguer, Jose (2014-08)
    Conditional rewriting modulo axioms with rich types makes specifications and declarative programs very expressive and succinct and is used in all well-known rule-based languages. However, the current foundations of ...

    application/pdf

    application/pdfPDF (564Kb)
  • Hendrix, Joe; Ohsaki, Hitoshi; Meseguer, Jose (2005-09)
    Sufficient completeness means that enough equations have been specified, so that the functions of an equational specification are fully defined on all relevant data. This is important for both debugging and formal reasoning. ...

    application/pdf

    application/pdfPDF (337Kb)
  • Escobar, Santiago; Meseguer, Jose (2007-02)
    Rewriting is a general and expressive way of specifying concurrent systems, where concurrent transitions are axiomatized by rewrite rules. Narrowing is a complete symbolic method for model checking reachability properties. ...

    application/pdf

    application/pdfPDF (373Kb)
  • Meseguer, Jose (2007-02)
    This paper presents the temporal logic of rewriting TLR*. Syntactically, TLR* is a very simple extension of CTL* which just adds action atoms, in the form of spatial action patterns, to CTL*. Semantically and pragmatically, ...

    application/pdf

    application/pdfPDF (718Kb)
  • Duran, Francisco; Lucas, Salvador; Meseguer, Jose (2009-06-19)
    Rewriting with rules R modulo axioms E is a widely used technique in both rule-based programming languages and in automated deduction. Termination methods for rewriting systems modulo specific axioms E (e.g., associativi ...

    application/pdf

    application/pdfPDF (311Kb)
  • Lucas, Salvador; Meseguer, Jose (2007-02)
    The main goal of this paper is to apply rewriting termination technology .enjoying a quite mature set of termination results and tools. to the problem of proving automatically the termination of concurrent systems under ...

    application/pdf

    application/pdfPDF (374Kb)
  • Rocha, Camilo; Meseguer, Jose (2007-12)
    Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean ...

    application/pdf

    application/pdfPDF (411Kb)
  • Escobar, Santiago; Meseguer, Jose; Sasse, Ralf (2007-10)
    Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union E = \Delta \uplus B with B a set of axioms for which a finitary unification algorithm exists, and \Delta a set ...

    application/pdf

    application/pdfPDF (309Kb)