BibSLEIGH — Jose

Travelled to:

1 × Australia
1 × Brazil
1 × Canada
1 × Cyprus
1 × Finland
1 × Greece
1 × Ireland
1 × Japan
1 × Poland
1 × Serbia
1 × Singapore
1 × Sweden
1 × Switzerland
11 × USA
2 × Austria
2 × Denmark
2 × Estonia
2 × Germany
2 × Hungary
3 × France
3 × The Netherlands
5 × United Kingdom
6 × Italy
7 × Spain

Collaborated with:

P.C.Ölveczky F.Durán S.Escobar ∅ S.Lucas K.Bae N.Martí-Oliet M.Clavel J.A.Goguen S.Eker C.L.Talcott R.Sasse A.Boronat U.Montanari P.Thati P.Lincoln G.Rosu R.Bruni M.Katelman J.Hendrix J.Jouannaud M.Sun A.Farzan J.F.Quesada M.AlTurki K.Futatsugi R.Gutiérrez C.Rocha S.Keller A.Verdejo M.Palomino F.Schernhammer C.Braga X.Qian J.Eckhardt T.Mühlbauer M.Wirsing C.Meadows P.Narendran F.Yang S.Liu C.A.Muñoz B.Alarcón L.Sha R.Heckel H.Ohsaki G.A.Agha K.Sen A.Sridharanarayanan G.Denker P.Degano C.Kirchner H.Kirchner A.Bouhoula S.Santiago A.Al-Nayeem M.Alpuente P.Ojeda F.Chen C.d.O.Braga E.H.Haeusler P.D.Mosses K.Okada D.Kapur C.Lynch C.Marché X.Urbain M.Keaton S.Zabele M.Stehr H.Ishikawa T.Watanabe H.Nakashima Catherine A. Meadows S.L.0003 K.Santhanam Q.W.0017 I.Gupta S.Erbatur Z.Liu

Talks about:

rewrit (38) maud (35) logic (30) semant (23) specif (16) system (15) analysi (14) time (13) real (13) order (12)

Person: José Meseguer

DBLP: Meseguer:Jos=eacute=

Facilitated 2 volumes:

Contributed to:

2014

2013

2012

2011

2010

2012

2009

2008

2009

2007

2006

2007

2006

2005

2004

2005

2007

2003

2002

2001

2000

1999

1998

1996

2002

1993

1992

1990

1989

1988

1987

1985

1984

1982

1987

1997

2018

2016

Wrote 123 papers:

FM-2014-BaeOM #analysis #multi #semantics: Definition, Semantics, and Analysis of Multirate Synchronous AADL (KB, PCÖ, JM), pp. 94–109.
LOPSTR-2014-LucasMG #2d #dependence #framework #term rewriting: Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems (SL, JM, RG), pp. 113–130.
PPDP-2014-LucasM #declarative #logic #proving #source code #termination: Proving Operational Termination of Declarative Programs in General Logics (SL, JM), pp. 111–122.
PPDP-2014-YangEMMN #encryption #finite #unification: Theories of Homomorphic Encryption, Unification, and the Finite Variant Property (FY, SE, CM, JM, PN), pp. 123–133.
RTA-TLCA-2014-BaeM #abstraction: Predicate Abstraction of Rewrite Theories (KB, JM), pp. 61–76.
WRLA-2014-BaeM #infinity #model checking #using: Infinite-State Model Checking of LTLR Formulas Using Narrowing (KB, JM), pp. 113–129.
WRLA-2014-LiuOM #ad hoc #framework #maude #mobile #network #realtime: A Framework for Mobile Ad hoc Networks in Real-Time Maude (SL, PCÖ, JM), pp. 162–177.
WRLA-2014-LucasM #order #termination: Strong and Weak Operational Termination of Order-Sorted Rewrite Theories (SL, JM), pp. 178–194.
WRLA-2014-LucasM14a #2d #dependence #proving #termination: 2D Dependency Pairs for Proving Operational Termination of CTRSs (SL, JM), pp. 195–212.
WRLA-2014-RochaMM #analysis #smt: Rewriting Modulo SMT and Open System Analysis (CR, JM, CAM), pp. 247–262.
WRLA-2014-SunM #fault tolerance #specification: Formal Specification of Button-Related Fault-Tolerance Micropatterns (MS, JM), pp. 263–279.
CADE-2013-ErbaturEKLLMMNSS #analysis #encryption #paradigm #protocol #symmetry #unification: Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis (SE, SE, DK, ZL, CL, CM, JM, PN, SS, RS), pp. 231–248.
RTA-2013-BaeEM #infinity #logic #model checking #using: Abstract Logical Model Checking of Infinite-State Systems Using Narrowing (KB, SE, JM), pp. 81–96.
FASE-2012-BaeOMA #maude: The SynchAADL2Maude Tool (KB, PCÖ, JM, AAN), pp. 59–62.
FASE-2012-EckhardtMAMW: Stable Availability under Denial of Service Attacks through Formal Patterns (JE, TM, MA, JM, MW), pp. 78–93.
WRLA-2012-BaeM #locality #model checking: Model Checking LTLR Formulas under Localized Fairness (KB, JM), pp. 99–117.
WRLA-2012-GutierrezMR #axiom #order #similarity: Order-Sorted Equality Enrichments Modulo Axioms (RG, JM, CR), pp. 162–181.
WRLA-2012-WirsingEMM #analysis #architecture #design #maude: Design and Analysis of Cloud-Based Architectures with KLAIM and Maude (MW, JE, TM, JM), pp. 54–82.
CAV-2011-BaeM #ltl #model checking #parametricity: State/Event-Based LTL Model Checking under Parametric Generalized Fairness (KB, JM), pp. 132–148.
GT-VMT-2011-BoronatM #automation #case study #maude #uml: Automated Model Synchronization: A Case Study on UML with Maude (AB, JM).
PPDP-2011-EscobarKLMMNS #analysis #encryption #protocol #unification #using: Protocol analysis in Maude-NPA using unification modulo homomorphic encryption (SE, DK, CL, CM, JM, PN, RS), pp. 65–76.
PPDP-2011-SchernhammerM #axiom #incremental #recursion #specification: Incremental checking of well-founded recursive specifications modulo axioms (FS, JM), pp. 5–16.
RTA-2011-DuranEEMT #maude #reachability #unification: Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6 (FD, SE, SE, JM, CLT), pp. 31–40.
WRLA-2010-AlarconLM #dependence #framework: A Dependency Pair Framework for A OR C-Termination (BA, SL, JM), pp. 35–51.
WRLA-2010-BaeM #linear #logic #maude #model checking: The Linear Temporal Logic of Rewriting Maude Model Checker (KB, JM), pp. 208–225.
WRLA-2010-DuranM #equation #maude #order #specification: A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications (FD, JM), pp. 69–85.
WRLA-2010-DuranM10a #maude #order: A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories (FD, JM), pp. 86–103.
WRLA-2010-EscobarSM #termination: Folding Variant Narrowing and Optimal Variant Termination (SE, RS, JM), pp. 52–68.
WRLA-2010-KatelmanKM #analysis #concurrent #semantics: Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits (MK, SK, JM), pp. 140–156.
WRLA-2010-Meseguer #logic: Twenty Years of Rewriting Logic (JM), pp. 15–17.
WRLA-2010-SunMS #architecture: A Formal Pattern Architecture for Safe Medical Systems (MS, JM, LS), pp. 157–173.
WRLA-J-2010-DuranM12 #on the #order: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories (FD, JM), pp. 816–850.
WRLA-J-2010-EscobarSM12 #termination: Folding variant narrowing and optimal variant termination (SE, RS, JM), pp. 898–928.
WRLA-J-2010-KatelmanKM12 #semantics #set: Rewriting semantics of production rule sets (MK, SK, JM), pp. 929–956.
WRLA-J-2010-Meseguer12 #logic: Twenty years of rewriting logic (JM), pp. 721–781.
FASE-2009-BoronatHM #logic #model transformation #semantics #verification: Rewriting Logic Semantics and Verification of Model Transformations (AB, RH, JM), pp. 18–33.
RTA-2009-ClavelDEELMMT #maude #unification: Unification and Narrowing in Maude 2.4 (MC, FD, SE, SE, PL, NMO, JM, CLT), pp. 380–390.
TOOLS-EUROPE-2009-BoronatM #algebra #metamodelling #ocl #semantics #specification: Algebraic Semantics of OCL-Constrained Metamodel Specifications (AB, JM), pp. 96–115.
FASE-2008-BoronatM #algebra #semantics: An Algebraic Semantics for MOF (AB, JM), pp. 377–391.
IJCAR-2008-DuranLM #maude #named #termination: MTT: The Maude Termination Tool (FD, SL, JM), pp. 313–319.
LOPSTR-2008-AlpuenteEMO #algorithm #composition #equation: A Modular Equational Generalization Algorithm (MA, SE, JM, PO), pp. 24–39.
PPDP-2008-LucasM #dependence #order: Order-sorted dependency pairs (SL, JM), pp. 108–119.
RTA-2008-EscobarMS #effectiveness #finite: Effectively Checking the Finite Variant Property (SE, JM, RS), pp. 79–93.
TACAS-2008-OlveczkyM #maude #realtime: The Real-Time Maude Tool (PCÖ, JM), pp. 332–336.
WRLA-2008-EscobarMS09 #equation #unification: Variant Narrowing and Equational Unification (SE, JM, RS), pp. 103–119.
WRLA-2008-LucasM09 #equation #order #source code #termination: Operational Termination of Membership Equational Programs: the Order-Sorted Way (SL, JM), pp. 207–225.
WRLA-2008-Marti-OlietMV09 #maude #semantics: A Rewriting Semantics for Maude Strategies (NMO, JM, AV), pp. 227–247.
PPDP-2007-AlTurkiM #realtime #semantics: Real-time rewriting semantics of orc (MA, JM), pp. 131–142.
RTA-2007-EscobarM #infinity #model checking #using: Symbolic Model Checking of Infinite-State Systems Using Narrowing (SE, JM), pp. 153–168.
RTA-2007-HendrixM #on the #order #specification: On the Completeness of Context-Sensitive Order-Sorted Specifications (JH, JM), pp. 229–245.
IJCAR-2006-HendrixMO #axiom #linear #order #specification: A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms (JH, JM, HO), pp. 151–155.
WRLA-2006-FarzanM07 #partial order #programming language #reduction #semantics: Partial Order Reduction for Rewriting Semantics of Programming Languages (AF, JM), pp. 61–78.
WRLA-2006-KatelmanM07 #analysis #co-evolution #design #hardware #semantics: A Rewriting Semantics for ABEL with Applications to Hardware/Software Co-Design and Analysis (MK, JM), pp. 47–60.
WRLA-2006-OlveczkyM07a #abstraction #maude #realtime: Abstraction and Completeness for Real-Time Maude (PCÖ, JM), pp. 5–27.
WRLA-2006-SasseM07 #algebra #hoare #java #logic #semantics #verification: Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics (RS, JM), pp. 29–46.
QAPL-2005-AghaMS06 #named #object-oriented #probability #specification: PMaude: Rewrite-based Specification Language for Probabilistic Object Systems (GAA, JM, KS), pp. 213–239.
RTA-2005-EscobarMT #term rewriting: Natural Narrowing for General Term Rewriting Systems (SE, JM, PT), pp. 279–293.
RTA-2005-HendrixCM #reasoning #specification: A Sufficient Completeness Reasoning Tool for Partial Specifications (JH, MC, JM), pp. 165–174.
RTA-2005-Meseguer #locality #semantics: Localized Fairness: A Rewriting Semantics (JM), pp. 250–263.
CAV-2004-FarzanCMR #analysis #formal method #java #source code: Formal Analysis of Java Programs in JavaFAN (AF, FC, JM, GR), pp. 501–505.
FASE-2004-OlveczkyM #analysis #maude #realtime #specification #using: Specification and Analysis of Real-Time Systems Using Real-Time Maude (PCÖ, JM), pp. 354–358.
IJCAR-2004-MeseguerR #analysis #formal method #logic #semantics #specification #tool support: Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools (JM, GR), pp. 1–44.
LOPSTR-2004-EscobarMT #term rewriting: Natural Rewriting for General Term Rewriting Systems (SE, JM, PT), pp. 101–116.
PEPM-2004-DuranLMMU #equation #proving #source code #termination: Proving termination of membership equational programs (FD, SL, JM, CM, XU), pp. 147–158.
WRLA-2004-BragaM05 #composition #semantics: Modular Rewriting Semantics in Practice (CB, JM), pp. 393–416.
WRLA-2004-Marti-OlietMV05 #maude #towards: Towards a Strategy Language for Maude (NMO, JM, AV), pp. 417–441.
WRLA-2004-MeseguerT05 #analysis #encryption #protocol #reachability #using #verification: Symbolic Reachability Analysis Using Narrowing and its Application to Verification of Cryptographic Protocols (JM, PT), pp. 153–182.
WRLA-2004-OlveczkyM05 #maude #realtime: Real-Time Maude 2.1 (PCÖ, JM), pp. 285–314.
WRLA-J-2004-MeseguerT07 #analysis #encryption #protocol #reachability #using #verification: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols (JM, PT), pp. 123–160.
WRLA-J-2004-OlveczkyM07 #maude #realtime #semantics: Semantics and pragmatics of Real-Time Maude (PCÖ, JM), pp. 161–196.
CADE-2003-MeseguerPM #abstraction #equation: Equational Abstractions (JM, MP, NMO), pp. 2–16.
FME-2003-RosuELM #equation #proving: Certifying and Synthesizing Membership Equational Proofs (GR, SE, PL, JM), pp. 359–380.
ICALP-2003-BruniM: Generalized Rewrite Theories (RB, JM), pp. 252–266.
RTA-2003-ClavelDELMMT #maude: The Maude 2.0 System (MC, FD, SE, PL, NMO, JM, CLT), pp. 76–87.
ECOOP-2002-MeseguerT #distributed #modelling #semantics: Semantic Models for Distributed Object Reflection (JM, CLT), pp. 1–36.
ICALP-2002-MeseguerR #algebra #approach #specification: A Total Approach to Partial Algebraic Specification (JM, GR), pp. 572–584.
LOPSTR-2002-BragaHMM #composition #logic: Mapping Modular SOS to Rewriting Logic (CdOB, EHH, JM, PDM), pp. 262–277.
WRLA-2002-BruniMM #logic #transaction: Tiling Transactions in Rewriting Logic (RB, JM, UM), pp. 90–109.
WRLA-2002-ClavelMP #equation #logic #similarity: Reflection in Membership Equational Logic, Many-Sorted Equational Logic, Horn Logic with Equality, and Rewriting Logic (MC, JM, MP), pp. 110–126.
WRLA-2002-EkerMS #ltl #maude #model checking: The Maude LTL Model Checker (SE, JM, AS), pp. 162–187.
FASE-2001-OlveczkyKMTZ #analysis #maude #network #protocol #realtime #specification: Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude (PCÖ, MK, JM, CLT, SZ), pp. 333–348.
FASE-2000-ClavelDELMMQ #maude #using: Using Maude (MC, FD, SE, PL, NMO, JM, JFQ), pp. 371–374.
RTA-2000-Meseguer #concept #logic #maude: Rewriting Logic and Maude: Concepts and Applications (JM), pp. 1–26.
WRLA-2000-ClavelDELMMQ #maude #towards: Towards Maude 2.0 (MC, FD, SE, PL, NMO, JM, JFQ), pp. 294–315.
WRLA-2000-DenkerMT #composition #distributed #semantics: Rewriting Semantics of Meta-Objects and Composable Distributed Services (GD, JM, CLT), pp. 405–425.
WRLA-2000-DuranM #maude: Parameterized Theories and Views in Full Maude 2.0 (FD, JM), pp. 316–338.
WRLA-2000-OlveczkyM #hybrid #maude #realtime #simulation: Real-Time Maude: A Tool for Simulating and Analyzing Real-Time and Hybrid Systems (PCÖ, JM), pp. 361–382.
FASE-1999-BruniMM #calculus #execution #process #specification: Executable Tile Specifications for Process Calculi (RB, JM, UM), pp. 60–76.
FM-v2-1999-ClavelDEMS #maude: Maude as a Formal Meta-tool (MC, FD, SE, JM, MOS), pp. 1684–1703.
RTA-1999-ClavelDELMMQ #maude: The Maude System (MC, FD, SE, PL, NMO, JM, JFQ), pp. 240–243.
FLOPS-1998-IshikawaWFMN #on the #semantics: On the Semantics of GAEA (HI, TW, KF, JM, HN), pp. 123–142.
WRLA-1998-BruniMM #implementation: Internal strategies in a rewriting implementation of tile systems (RB, JM, UM), pp. 263–284.
WRLA-1998-ClavelDELMM #maude: Metalevel computation in Maude (MC, FD, SE, PL, NMO, JM), pp. 331–352.
WRLA-1998-ClavelDELMMQ #maude #metalanguage: Maude as a metalanguage (MC, FD, SE, PL, NMO, JM, JFQ), pp. 147–160.
WRLA-1998-DuranM #algebra #maude: An extensible module algebra for Maude (FD, JM), pp. 174–195.
WRLA-1998-MeseguerT #logic: Mapping OMRS to rewriting logic (JM, CLT), pp. 33–54.
RWLW-1996-ClavelELM #maude: Principles of Maude (MC, SE, PL, JM), pp. 65–89.
RWLW-1996-ClavelM #logic: Reflection and strategies in rewriting logic (MC, JM), pp. 126–148.
RWLW-1996-Marti-OlietM #framework #logic #semantics: Rewriting logic as a logical and semantic framework (NMO, JM), pp. 190–225.
RWLW-1996-OlveczkyM #logic #realtime #specification: Specifying real-time systems in rewriting logic (PCÖ, JM), pp. 284–309.
WRLA-J-1996-ClavelDELMMQ02 #logic #maude #named #programming #specification: Maude: specification and programming in rewriting logic (MC, FD, SE, PL, NMO, JM, JFQ), pp. 187–243.
WRLA-J-1996-ClavelM02 #logic: Reflection in conditional rewriting logic (MC, JM), pp. 245–288.
WRLA-J-1996-Marte-OlietM02 #logic #overview #roadmap: Rewriting logic: roadmap and bibliography (NMO, JM), pp. 121–154.
WRLA-J-1996-OlveczkyM02 #hybrid #logic #realtime #specification: Specification of real-time and hybrid systems in rewriting logic (PCÖ, JM), pp. 359–405.
ECOOP-1993-Meseguer #concurrent #inheritance #object-oriented #programming: Solving the Inheritance Anomaly in Concurrent Object-Oriented Programming (JM), pp. 220–246.
SIGMOD-1993-MeseguerQ #database #logic #object-oriented #semantics: A Logical Semantics for Object-Oriented Databases (JM, XQ), pp. 89–98.
ALP-1992-Meseguer #logic programming #multi #paradigm: Multiparadigm Logic Programming (JM), pp. 158–200.
OOPSLA-ECOOP-1990-Meseguer #concurrent #logic: A Logical Theory of Concurrent Objects (JM), pp. 101–115.
LICS-1989-DeganoMM #axiom #process: Axiomatizing Net Computations and Processes (PD, JM, UM), pp. 175–185.
POPL-1989-Meseguer #modelling #morphism #polymorphism: Relating Models of Polymorphism (JM), pp. 228–241.
ICALP-1988-KirchnerKM #semantics: Operational Semantics of OBJ-3 (CK, HK, JM), pp. 287–301.
LICS-1988-MeseguerM #algebra #monad #petri net: Petri Nets Are Monoids: A New Algebraic Foundation for Net Theory (JM, UM), pp. 155–164.
ICSE-1987-FutatsugiGMO #programming: Parameterized Programming in OBJ2 (KF, JAG, JM, KO), pp. 51–60.
LICS-1987-GoguenM #algebra #multi #order: Order-Sorted Algebra solves the Constructor-Selector, Multiple (JAG, JM), pp. 18–29.
ICALP-1985-GoguenJM #algebra #order #semantics: Operational Semantics for Order-Sorted Algebra (JAG, JPJ, JM), pp. 221–231.
POPL-1985-FutatsugiGJM: Principles of OBJ2 (KF, JAG, JPJ, JM), pp. 52–66.
ILPC-1984-GoguenM84 #logic programming #similarity: Equality, Types, Modules and Generics for Logic Programming (JAG, JM), pp. 115–125.
ICALP-1982-GoguenM #implementation #persistent: Universal Realization, Persistent Interconnection and Implementation of Abstract Modules (JAG, JM), pp. 265–281.
AF-1987-GoguenM #logic #modelling #programming #similarity: Models and Equality for Logical Programming (JAG, JM), pp. 1–22.
TAPSOFT-1997-BouhoulaJM #equation #logic #proving #specification: Specification and Proof in Membership Equational Logic (AB, JPJ, JM), pp. 67–92.
FASE-2018-LiuOSWGM #analysis #distributed #formal method #named #protocol #transaction: ROLA: A New Distributed Transaction Protocol and Its Formal Analysis (SL0, PCÖ, KS, QW0, IG, JM), pp. 77–93.
IJCAR-2016-DuranEEMMT #generative #maude #unification: Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 (FD, SE, SE, NMO, JM, CLT), pp. 183–192.
PPDP-2016-YangEMMS #algebra #process #semantics: Strand spaces with choice via a process algebra semantics (FY, SE, CAM, JM, SS), pp. 76–89.