Find Research Outputs

Search in all content

Filters for Research & Scholarship

Search concepts
Selected Filters

Publication Year

  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011

Author

  • Jose Meseguer

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

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. Fioravanti, F. & Gallagher, J. P. (eds.). Springer-Verlag Berlin Heidelberg, 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

A Constructor-Based Reachability Logic for Rewrite Theories

Skeirik, S., Stefanescu, A. & Meseguer, J., Jan 1 2020, In : Fundamenta Informaticae. 173, 4, p. 315-382 68 p.

Research output: Contribution to journalArticle

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 Berlin Heidelberg, 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

A modular order-sorted equational generalization algorithm

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

Research output: Contribution to journalArticle

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. Chen, L. & Mitchell, C. (eds.). Springer-Verlag Berlin Heidelberg, 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

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

A partial evaluation framework for order-sorted equational programs modulo axioms

Alpuente, M., Cuenca-Ortega, A., Escobar, S. & Meseguer, J., Jan 2020, In : Journal of Logical and Algebraic Methods in Programming. 110, 100501.

Research output: Contribution to journalArticle

Open Access

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

A rewriting-based model checker for the linear temporal logic of rewriting

Bae, K. & Meseguer, J., Dec 20 2012, In : Electronic Notes in Theoretical Computer Science. 290, p. 19-36 18 p.

Research output: Contribution to journalArticle

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 Berlin Heidelberg, 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

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

Automated model synchronization: A case study on UML with Maude

Boronat, A. & Meseguer, J., Jan 1 2011, In : Electronic Communications of the EASST. 41

Research output: Contribution to journalArticle

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. Zhang, L. & Vojnar, T. (eds.). Springer-Verlag Berlin Heidelberg, 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

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

Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method

Escobar, S. & Meseguer, J., 2019, Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows. Guttman, J. D., Landwehr, C. E., Meseguer, J. & Pavlovic, D. (eds.). Springer-Verlag Berlin Heidelberg, 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

Constrained narrowing for conditional equational theories modulo axioms

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

Research output: Contribution to journalArticle

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

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

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

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

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

Enhancing safety and security of distributed systems through formal patterns

Eckhardt, J., M̈uhlbauer, T., Meseguer, J. & Wirsing, M., Dec 1 2012, In : CEUR Workshop Proceedings. 834, p. 35-40 6 p.

Research output: Contribution to journalConference article

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

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

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

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 Berlin Heidelberg, 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

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

Folding variant narrowing and optimal variant termination

Escobar, S., Sasse, R. & Meseguer, J., Oct 2012, In : Journal of Logic and Algebraic Programming. 81, 7-8, p. 898-928 31 p.

Research output: Contribution to journalArticle

Formal analysis of fault-tolerant group key management using ZooKeeper

Skeirik, S., Bobba, R. B. & Meseguer, J., Aug 14 2013, p. 636-641. 6 p.

Research output: Contribution to conferencePaper

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 Berlin Heidelberg, 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

Formalization and correctness of the PALS architectural pattern for distributed real-time systems

Meseguer, J. & Ölveczky, P. C., Sep 14 2012, In : Theoretical Computer Science. 451, p. 1-37 37 p.

Research output: Contribution to journalArticle

Formal Modeling Actors, Open Systems, Biological Systems: Essays dedicated to Carolyn Talcott on the occasion of her 70th birthday

Agha, G. A. (ed.), Danvy, O. (ed.) & Meseguer, J. (ed.), 2011, Berlin: Springer. (Lecture Notes in Computer Science; vol. 7000)

Research output: Book/Report/Conference proceedingAnthology

Formal modeling and analysis of cassandra in maude

Liu, S., Rahman, M. R., Skeirik, S., Gupta, I. & Meseguer, J., Jan 1 2014, Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings. Merz, S. & Pang, J. (eds.). Springer-Verlag, 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

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

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 Berlin Heidelberg, 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 patterns for multirate distributed real-time systems

Bae, K., Meseguer, J. & Ölveczky, P. C., Oct 1 2014, In : Science of Computer Programming. 91, PART A, p. 3-44 42 p.

Research output: Contribution to journalArticle

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

Open Access

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 Berlin Heidelberg, 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

Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs

Liu, S., Sandur, A., Meseguer, J., Ölveczky, P. C. & Wang, Q., 2020, NASA Formal Methods - 12th International Symposium, NFM 2020, Proceedings. Lee, R., Jha, S. & Mavridou, A. (eds.). Springer, p. 22-40 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12229 LNCS).

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

Ground confluence of order-sorted conditional specifications modulo axioms

Durán, F., Meseguer, J. & Rocha, C., Feb 2020, In : Journal of Logical and Algebraic Methods in Programming. 111, 100513.

Research output: Contribution to journalArticle

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 Berlin Heidelberg, 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

IBOS: A correct-by-construction modular browser

Sasse, R., King, S. T., Meseguer, J. & Tang, S., Jan 28 2013, Formal Aspects of Component Software - 9th International Symposium, FACS 2012, Revised Selected Papers. 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