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

Research Output 1975 2019

Filter
Conference contribution
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
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

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
2017

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
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

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

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

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

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
2014

Analysis of the ibm cca security api protocols in maude-npa

González-Burgueño, A., Santiago, S., Escobar, S., Meadows, C. & Meseguer, J., 2014, Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings. Springer Verlag, Vol. 8893. p. 111-130 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8893).

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

Maude
Security Protocols
Application programming interfaces (API)
Network protocols
Cryptographic Protocols

A rewriting-based forwards semantics for Maude-NPA

Escobar, S., Meadows, C., Meseguer, J. & Santiago, S., Jan 1 2014, Proceedings of the 2014 Symposium and Bootcamp on the Science of Security, HotSoS 2014. Association for Computing Machinery, 3. (ACM International Conference Proceeding Series).

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

Semantics
Network protocols
Model checking
Authentication
Cryptography

Definition, semantics, and analysis of multirate synchronous AADL

Bae, K., Ölveczky, P. C. & Meseguer, J., Jan 1 2014, FM 2014: Formal Methods - 19th International Symposium, Proceedings. Springer-Verlag, p. 94-109 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8442 LNCS).

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

Semantics
Maude
Distributed parameter control systems
Model checking
Explosions

Formal modeling and analysis of cassandra in maude

Liu, S., Rahman, M. R., Skeirik, S., Gupta, I. & Meseguer, J., 2014, Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings. Springer Verlag, Vol. 8829. p. 332-347 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8829).

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

Maude
Formal Modeling
Formal Analysis
Latency
Formal Model

Models for logics and conditional constraints in automated proofs of termination

Lucas, S. & Meseguer, J., Jan 1 2014, Artificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Proceedings. Calmet, J., Aranda-Corral, G. A. & Martín-Mateos, F. J. (eds.). Springer-Verlag, p. 9-20 12 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8884).

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

Termination
Logic
Numerics
Linear algebra
Real Algebraic Geometry

Predicate abstraction of rewrite theories

Bae, K. & Meseguer, J., Jan 1 2014, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer-Verlag, p. 61-76 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8560 LNCS).

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

Predicate
Formal Specification
Semantics
Concretes
Automated Deduction

Proving operational termination of declarative programs in general logics

Lucas, S. & Meseguer, J., Sep 8 2014, PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery, Inc, p. 111-122 12 p. (PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming).

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

Schematic diagrams
Semantics

Theories of homomorphic encryption, unification, and the finite variant property

Yang, F., Escobar, S., Meadows, C., Meseguer, J. & Narendran, P., Sep 8 2014, PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming. Association for Computing Machinery, Inc, p. 123-134 12 p. (PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming).

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

Cryptography
Network protocols
Decomposition
2013

Abstract logical model checking of infinite-state systems using narrowing

Bae, K., Escobar, S. & Meseguer, J., Jan 1 2013, 24th International Conference on Rewriting Techniques and Applications, RTA 2013. van Raamsdonk, F. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 81-96 16 p. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 21).

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

Model checking
Algebra

Asymmetric unification: A new unification paradigm for cryptographic protocol analysis

Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C. A., Meadows, C., Meseguer, J., Narendran, P., Santiago, S. & Sasse, R., Jul 15 2013, CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. p. 231-248 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7898 LNAI).

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

Cryptographic Protocols
Unification
Paradigm
Network protocols
Computability and decidability

Formal analysis of fault-tolerant group key management using ZooKeeper

Skeirik, S., Bobba, R. B. & Meseguer, J., 2013, Proceedings - 13th IEEE/ACM International Symposium on Cluster, Cloud, and Grid Computing, CCGrid 2013. p. 636-641 6 p. 6546150

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

Model checking
Viruses
Managers
Statistical Models

Formal patterns for multi-rate distributed real-time systems

Bae, K., Meseguer, J. & Ölveczky, P. C., Jan 28 2013, Formal Aspects of Component Software - 9th International Symposium, FACS 2012, Revised Selected Papers. p. 1-18 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7684 LNCS).

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

Real time systems
Distributed Systems
Ailerons
Real-time
Control systems

IBOS: A correct-by-construction modular browser

Sasse, R., King, S. T., Meseguer, J. & Tang, S., 2013, Formal Aspects of Component Software - 9th International Symposium, FACS 2012, Revised Selected Papers. Vol. 7684 LNCS. p. 224-241 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7684 LNCS).

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

Modular construction
Web browsers
Trusted Computing
Rewriting Logic
Formal Specification

Statistical model checking for composite actor systems

Eckhardt, J., Mühlbauer, T., Meseguer, J. & Wirsing, M., Jul 17 2013, Recent Trends in Algebraic Development Techniques - 21st International Workshop, WADT 2012, Revised Selected Papers. p. 143-160 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7841 LNCS).

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

Model checking
Model Checking
Statistical Model
Composite
Bisimulation
2012

Design and analysis of cloud-based architectures with KLAIM and Maude

Wirsing, M., Eckhardt, J., Mühlbauer, T. & Meseguer, J., Nov 8 2012, Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers. p. 54-82 29 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7571 LNCS).

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

Maude
Security systems
Composite materials
Model checking
Cloud computing

Effective symbolic protocol analysis via equational irreducibility conditions

Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Santiago, S. & Sasse, R., Sep 5 2012, Computer Security, ESORICS 2012 - 17th European Symposium on Research in Computer Security, Proceedings. p. 73-90 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7459 LNCS).

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

Irreducibility
Unification
Symbolic Analysis
Reachability Analysis
Cryptography

Model checking LTLR formulas under localized fairness

Bae, K. & Meseguer, J., Nov 8 2012, Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers. p. 99-117 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7571 LNCS).

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

Temporal logic
Model checking
Fairness
Model Checking
Temporal Logic

Order-sorted equality enrichments modulo axioms

Gutiérrez, R., Meseguer, J. & Rocha, C., Nov 8 2012, Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Revised Selected Papers. p. 162-181 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7571 LNCS).

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

Algebraic Specification
Predicate
Axioms
Modulo
Equality

Stable availability under denial of service attacks through formal patterns

Eckhardt, J., Mühlbauer, T., Alturki, M., Meseguer, J. & Wirsing, M., Apr 3 2012, Fundamental Approaches to Software Engineering - 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. p. 78-93 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7212 LNCS).

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

Denial of Service
Availability
Attack
Servers
Server

State space c-reductions of concurrent systems in rewriting logic

Lluch Lafuente, A., Meseguer, J. & Vandin, A., Dec 1 2012, Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods, ICFEM 2012, Proceedings. p. 430-446 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7635 LNCS).

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

Rewriting Logic
Concurrent Systems
State Space
Maude
Proof of correctness

Taming distributed system complexity through formal patterns

Meseguer, J., Dec 31 2012, Formal Aspects of Component Software - 8th International Symposium, FACS 2011, Revised Selected Papers. p. 1-2 2 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7253 LNCS).

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

Distributed Systems
Safety
Real-time
Requirements

The synchAADL2Maude tool

Bae, K., Ölveczky, P. C., Meseguer, J. & Al-Nayeem, A., Apr 3 2012, Fundamental Approaches to Software Engineering - 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. p. 59-62 4 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7212 LNCS).

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

Modeling
Real time systems
Synchronous Systems
Real-time
Maude
2011

Incremental checking of well-founded recursive specifications modulo axioms

Schernhammer, F. & Meseguer, J., Sep 2 2011, PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. p. 5-16 12 p. (PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming).

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

Axioms
Modulo
Commutativity
Specification
Specifications