1975 …2019
If you made any changes in Pure, your changes will be visible here soon.

Research Output 1975 2019

2019

ACUOS2: A High-Performance System for Modular ACU Generalization with Subtyping and Inheritance

Alpuente, M., Ballis, D., Cuenca-Ortega, A., Escobar, S. & Meseguer, J., Jan 1 2019, Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Proceedings. Calimeri, F., Leone, N. & Manna, M. (eds.). Springer-Verlag, p. 171-181 11 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11468 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

High Performance
Artificial intelligence
Associativity
Computing
Multiset

Automatic analysis of consistency properties of distributed transaction systems in maude

Liu, S., Ölveczky, P. C., Zhang, M., Wang, Q. & Meseguer, J., Jan 1 2019, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Vojnar, T. & Zhang, L. (eds.). Springer-Verlag, p. 40-57 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11428 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
Maude
Model checking
Fault tolerance
Transactions
Scalability

Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method

Escobar, S. & Meseguer, J., Jan 1 2019, Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows. Meseguer, J., Landwehr, C. E., Pavlovic, D. & Guttman, J. D. (eds.). Springer-Verlag, p. 15-38 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11565 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Irreducibility
Symbolic Analysis
Maude
Reachability Analysis
Equational Theory

Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms

Alpuente, M., Cuenca-Ortega, A., Escobar, S. & Meseguer, J., Jan 1 2019, Logic-Based Program Synthesis and Transformation - 28th International Symposium, LOPSTR 2018. Stuckey, P. J. & Mesnard, F. (eds.). Springer-Verlag, p. 38-55 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11408 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Associativity
Commutativity
Homeomorphic
Axioms
Modulo

Preface

Guttman, J., Landwehr, C., Meseguer, J. & Pavlovic, D., Jan 1 2019, In : Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 11565 LNCS, p. vii-ix

Research output: Contribution to journalEditorial

2018

A constructor-based reachability logic for rewrite theories

Skeirik, S., Stefanescu, A. & Meseguer, J., Jan 1 2018, Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. Springer-Verlag, p. 201-217 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10855 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Reachability
Semantics
Systems analysis
Acoustic waves
Logic

Associative unification and symbolic reasoning modulo associativity in maude

Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J. & Talcott, C., Jan 1 2018, Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. Rusu, V. (ed.). Springer-Verlag, p. 98-114 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11152 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Maude
Associativity
Unification
Modulo
Reasoning

Formal design of cloud computing systems in maude

Meseguer, J., Jan 1 2018, Formal Methods: Foundations and Applications - 21st Brazilian Symposium, SBMF 2018, Proceedings. Massoni, T. & Mousavi, M. R. (eds.). Springer-Verlag, p. 5-19 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11254 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Maude
Cloud computing
Cloud Computing
Computer systems
Distributed Systems

Formal modeling and analysis of the walter transactional data store

Liu, S., Ölveczky, P. C., Wang, Q. & Meseguer, J., Jan 1 2018, Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. Rusu, V. (ed.). Springer-Verlag, p. 136-152 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11152 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Formal Modeling
Formal Analysis
Model checking
Maude
Snapshot

Generalized rewrite theories and coherence completion

Meseguer, J., Jan 1 2018, Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. Rusu, V. (ed.). Springer-Verlag, p. 164-183 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11152 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Completion
Reasoning
Requirements
Standards

Modular Verification of Sequential Composition for Private Channels in Maude-NPA

Yang, F., Escobar, S., Meadows, C. & Meseguer, J., Jan 1 2018, Security and Trust Management - 14th International Workshop, STM 2018, Proceedings. Alcaraz, C., Katsikas, S. K. & Katsikas, S. K. (eds.). Springer-Verlag, p. 20-36 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11091 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Maude
Network protocols
Chemical analysis
Equational Theory
Cryptographic Protocols

Proving ground confluence of equational specifications modulo axioms

Durán, F., Meseguer, J. & Rocha, C., Jan 1 2018, Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. Rusu, V. (ed.). Springer-Verlag, p. 184-204 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11152 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Confluence
Axioms
Modulo
Specification
Specifications

ROLA: A new distributed transaction protocol and its formal analysis

Liu, S., Ölveczky, P. C., Santhanam, K., Wang, Q., Gupta, I. & Meseguer, J., Jan 1 2018, Fundamental Approaches to Software Engineering - 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Schurr, A. & Russo, A. (eds.). Springer-Verlag, p. 77-93 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10802 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Formal Analysis
Model checking
Distributed database systems
Transactions
Network protocols

Symbolic reasoning methods in rewriting logic and maude

Meseguer, J., Jan 1 2018, Logic, Language, Information, and Computation - 25th International Workshop, WoLLIC 2018, Proceedings. Springer-Verlag, p. 25-60 36 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10944 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Rewriting Logic
Maude
Reasoning
Engines
Computer programming languages

The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors

Lucas, S., Meseguer, J. & Gutiérrez, R., Jan 1 2018, (Accepted/In press) In : Journal of Computer and System Sciences.

Research output: Contribution to journalArticle

Termination
Rewriting
Term Rewriting Systems
Framework
Horizontal

Variant-based decidable satisfiability in initial algebras with predicates

Gutiérrez, R. & Meseguer, J., Jan 1 2018, Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. Fioravanti, F. & Gallagher, J. P. (eds.). Springer-Verlag, p. 306-322 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10855 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Predicate
Algebra
Data structures
Decision Procedures
Data Structures

Variant-based satisfiability in initial algebras

Meseguer, J., Mar 1 2018, In : Science of Computer Programming. 154, p. 3-41 39 p.

Research output: Contribution to journalArticle

Algebra
Surface mount technology
2017

Dependency pairs for proving termination properties of conditional term rewriting systems

Lucas, S. & Meseguer, J., Jan 1 2017, In : Journal of Logical and Algebraic Methods in Programming. 86, 1, p. 236-268 33 p.

Research output: Contribution to journalArticle

Term Rewriting Systems
Termination
Semantics
Rewriting
Logic

Equational formulas and pattern operations in initial order-sorted algebras

Meseguer, J. & Skeirik, S., May 1 2017, In : Formal Aspects of Computing. 29, 3, p. 423-452 30 p.

Research output: Contribution to journalArticle

Algebra
Boolean Operation
Computability and decidability
First-order Logic
Decidability

Exploring Design Alternatives for RAMP Transactions Through Statistical Model, Checking

Liu, S., Ölveczky, P. C., Ganhotra, J., Gupta, I. & Meseguer, J., Jan 1 2017, Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings. Duan, Z. & Ong, L. (eds.). Springer-Verlag, p. 298-314 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10610 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Model checking
Model Checking
Statistical Model
Transactions
Partition

Partial evaluation of order-sorted equational programs modulo axioms

Alpuente, M., Cuenca-Ortega, A., Escobar, S. & Meseguer, J., Jan 1 2017, Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Revised Selected Papers. Hermenegildo, M. V. & Lopez-Garcia, P. (eds.). Springer-Verlag, p. 3-20 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10184 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Partial Evaluation
Axioms
Modulo
Maude
Commutativity

Rewriting modulo SMT and open system analysis

Rocha, C., Meseguer, J. & Muñoz, C., Jan 1 2017, In : Journal of Logical and Algebraic Methods in Programming. 86, 1, p. 269-297 29 p.

Research output: Contribution to journalArticle

Surface mount technology
Open systems
Open Systems
Rewriting
Systems Analysis

Strict coherence of conditional rewriting modulo axioms

Meseguer, J., Apr 11 2017, In : Theoretical Computer Science. 672, p. 1-35 35 p.

Research output: Contribution to journalArticle

Rewriting
Axioms
Modulo
Specifications
Termination
2016

Built-in variant generation and unification, and their applications in Maude 2.7

Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J. & Talcott, C., Jan 1 2016, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. Springer Verlag, Vol. 9706. p. 183-192 10 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9706).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Maude
Unification
Modulo
Associativity
Commutativity

Formal modeling and analysis of RAMP transaction systems

Liu, S., Ganhotra, J., Ölveczky, P. C., Gupta, I., Rahman, M. R. & Meseguer, J., Apr 4 2016, 2016 Symposium on Applied Computing, SAC 2016. Association for Computing Machinery, p. 1700-1707 8 p. (Proceedings of the ACM Symposium on Applied Computing; vol. 04-08-April-2016).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Model checking
Servers
Semantics

Metalevel algorithms for variant satisfiability

Skeirik, S. & Meseguer, J., Jan 1 2016, Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. Lucanu, D. (ed.). Springer-Verlag, p. 167-184 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9942 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Maude
Quantifiers
Algebra
Compactness

Modeling and analyzing mobile ad hoc networks in Real-Time Maude

Liu, S., Ölveczky, P. C. & Meseguer, J., Jan 1 2016, In : Journal of Logical and Algebraic Methods in Programming. 85, 1, p. 34-66 33 p.

Research output: Contribution to journalArticle

Maude
Mobile ad hoc networks
Mobile Ad Hoc Networks
Real-time
Communication Delay

Normal forms and normal theories in conditional rewriting

Lucas, S. & Meseguer, J., Jan 1 2016, In : Journal of Logical and Algebraic Methods in Programming. 85, 1, p. 67-97 31 p.

Research output: Contribution to journalArticle

Rewriting
Normal Form
Algebra
Semantics
Termination

Order-sorted rewriting and congruence closure

Meseguer, J., Jan 1 2016, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Löding, C. & Jacobs, B. (eds.). Springer-Verlag, p. 493-509 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9634).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Theorem proving
Rewriting
Polymorphism
Congruence
Closure

Strand spaces with choice via a process Algebra semantics

Yang, F., Escobar, S., Meadows, C., Meseguer, J. & Santiago, S., Sep 5 2016, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016. Association for Computing Machinery, Inc, p. 76-89 14 p. (Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Algebra
Semantics
Taxonomies

Towards generic monitors for object-oriented real-time maude specifications

Moreno-Delgado, A., Durán, F. & Meseguer, J., Jan 1 2016, Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. Lucanu, D. (ed.). Springer-Verlag, p. 134-151 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9942 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Maude
Object-oriented
Monitor
Specification
Specifications

Variant-based satisfiability in initial algebras

Meseguer, J., Jan 1 2016, Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers. Ölveczky, P. C. & Artho, C. (eds.). Springer-Verlag, p. 3-34 32 p. (Communications in Computer and Information Science; vol. 596).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Algebra
Unification
Surface mount technology
Decision Procedures
Folding
2015

Analysis of the PKCS#11 API using the maude-NPA tool

González-Burgueño, A., Santiago, S., Escobar, S., Meadows, C. & Meseguer, J., Jan 1 2015, Security Standardisation Research - 2nd International Conference, SSR 2015, Proceedings. Chen, L. & Matsuo, S. (eds.). Springer-Verlag, p. 86-106 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9497).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Maude
Application programming interfaces (API)
Network protocols
Smart Card
Public key

Constrained narrowing for conditional equational theories modulo axioms

Cholewa, A., Escobar, S. & Meseguer, J., Jan 1 2015, In : Science of Computer Programming. 112, P1, p. 24-57 34 p.

Research output: Contribution to journalArticle

Substitution reactions

Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study

Bae, K., Krisiloff, J., Meseguer, J. & Ölveczky, P. C., Jun 1 2015, In : Science of Computer Programming. 103, p. 13-50 38 p.

Research output: Contribution to journalArticle

Aircraft
Control systems
Model checking
Distributed parameter control systems
Aviation

Equational formulas and pattern operations in initial order-sorted algebras

Meseguer, J. & Skeirik, S., Jan 1 2015, Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers. Falaschi, M. (ed.). Springer-Verlag, p. 36-53 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9527).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Algebra
Computability and decidability
Polymorphism
Boolean Operation
First-order Logic

Executable rewriting logic semantics of Orc and formal analysis of Orc programs

Alturki, M. A. & Meseguer, J., Aug 8 2015, In : Journal of Logical and Algebraic Methods in Programming. 84, 4, p. 505-533 29 p., 42.

Research output: Contribution to journalArticle

Rewriting Logic
Formal Analysis
Semantics
Calculus
Maude

Extending the 2D dependency pair framework for conditional term rewriting systems

Lucas, S., Meseguer, J. & Gutiérrez, R., Jan 1 2015, Logic-Based Program Synthesis and Transformation - 24th International Symposium, LOPSTR 2014, Revised Selected Papers. Proietti, M. & Seki, H. (eds.). Springer-Verlag, p. 113-130 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8981).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Term Rewriting Systems
Termination
Rewriting
Term
Framework
Leader Election
Maude
Formal Analysis
Mobile ad hoc networks
Mobile Ad Hoc Networks
Termination
Computer programming languages
Logic
Programming Languages
Semantics

Model checking linear temporal logic of rewriting formulas under localized fairness

Bae, K. & Meseguer, J., Mar 1 2015, In : Science of Computer Programming. 99, p. 193-234 42 p.

Research output: Contribution to journalArticle

Temporal logic
Model checking
Specification languages
User interfaces

Order-sorted equality enrichments modulo axioms

Gutiérrez, R., Meseguer, J. & Rocha, C., Mar 1 2015, In : Science of Computer Programming. 99, p. 235-261 27 p.

Research output: Contribution to journalArticle

Specifications
Theorem proving
Algebra
Semantics

Quantitative analysis of consistency in NoSQL key-value stores

Liu, S., Nguyen, S., Ganhotra, J., Rahman, M. R., Gupta, I. & Meseguer, J., Jan 1 2015, Quantitative Evaluation of Systems - 12th International Conference, QEST 2015, Proceedings. Campos, J. & Haverkort, B. R. (eds.). Springer-Verlag, p. 228-243 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9259).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Quantitative Analysis
Model checking
Chemical analysis
Probabilistic Model
Model Checking

Semantics, distributed implementation, and formal analysis of KLAIM models in Maude

Eckhardt, J., Mühlbauer, T., Meseguer, J. & Wirsing, M., Mar 1 2015, In : Science of Computer Programming. 99, p. 24-74 51 p.

Research output: Contribution to journalArticle

Semantics
Specifications
Temporal logic
Model checking
Algebra

Symbolic protocol analysis with disequality constraints modulo equational theories

Escobar, S., Meadows, C., Meseguer, J. & Santiago, S., Jan 1 2015, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag, p. 238-261 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9465).

Research output: Chapter in Book/Report/Conference proceedingChapter

Equational Theory
Algebra
Modulo
Cryptographic Protocols
Formal Analysis
2014
Term Rewriting Systems
Termination
Rewriting
Reachability
Sequencing
Axioms
Artificial intelligence
Data structures
Reasoning
Semantics
Maude
Network protocols
Algebraic Theory
Cryptographic Protocols
Modulo
Maude
Mobile ad hoc networks
Mobile Ad Hoc Networks
Mobility Model
Real-time

A modular order-sorted equational generalization algorithm

Alpuente, M., Escobar, S., Espert, J. & Meseguer, J., Jan 1 2014, In : Information and Computation. 235, p. 98-136 39 p.

Research output: Contribution to journalArticle

Axioms
Unification
Theorem proving
Program Synthesis
Partial Evaluation