Find Research Outputs

Search concepts
Selected Filters
2010

A church-rosser checker tool for conditional order-sorted equational maude specifications

Durán, F. & Meseguer, J., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 69-85 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Maude
Religious buildings
Associativity
Commutativity
Axioms

A dependency pair framework for AVC-termination

Alarcón, B., Lucas, S. & Meseguer, J., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 35-51 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Termination
Computer programming languages
Rewriting
Equational Theory
Modulo

A formal executable semantics of verilog

Meredith, P., Katelman, M., Meseguer, J. & Rosu, G., Oct 15 2010, 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010. p. 179-188 10 p. 5558634. (8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010).

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

Computer hardware description languages
Semantics
Simulators

A formal pattern architecture for safe medical systems

Sun, M., Meseguer, J. & Sha, L. R., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 157-173 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Pacemakers
Safety
Rewriting Logic
Maude
Safety-critical Systems

Algebraic simulations

Meseguer, J., Palomino, M. & Martí-Oliet, N., Feb 1 2010, In : Journal of Logic and Algebraic Programming. 79, 2, p. 103-143 41 p.

Research output: Contribution to journalArticle

Temporal logic
Theorem proving
Rewriting Logic
Concurrent Systems
Temporal Logic

A maude coherence checker tool for conditional order-sorted rewrite theories

Durán, F. & Meseguer, J., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 86-103 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Maude
Axioms
Modulo
Associativity
Commutativity

An algebraic semantics for MOF

Boronat, A. & Meseguer, J., May 1 2010, In : Formal Aspects of Computing. 22, 3-4, p. 269-296 28 p.

Research output: Contribution to journalArticle

Algebraic Semantics
Semantics
Metamodel
Equational Logic
Formal Semantics

Concurrent rewriting semantics and analysis of asynchronous digital circuits

Katelman, M., Keller, S. & Meseguer, J., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 140-156 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Asynchronous Circuits
Production Rules
Digital Circuits
Digital circuits
Rewriting

Constructors, sufficient completeness, and deadlock freedom of rewrite theories

Rocha, C. & Meseguer, J., Nov 23 2010, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. Fermuller, C. G. (ed.). p. 594-609 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6397 LNCS).

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

Deadlock
Completeness
Sufficient
Specifications
Maude

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Rocha, C. & Meseguer, J., Jan 1 2010, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. Fermuller, C. G. & Voronkov, A. (eds.). Springer-Verlag, p. 594-609 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6397 LNCS).

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

Deadlock
Completeness
Sufficient
Specifications
Maude

Coverset induction with partiality and subsorts: A powerlist case study

Hendrix, J., Kapur, D. & Meseguer, J., Aug 10 2010, Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. p. 275-290 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6172 LNCS).

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

Proof by induction
Formal logic
Recursive functions
Specifications
Maude

Folding variant narrowing and optimal variant termination

Escobar, S., Sasse, R. & Meseguer, J., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 52-68 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Folding
Termination
Modulo
Computing
Term

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

Meseguer, J. & Ölveczky, P. C., Dec 6 2010, Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings. p. 303-320 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6447 LNCS).

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

Real time systems
Formalization
Distributed Systems
Correctness
Real-time

Formal semantics and analysis of behavioral AADL models in real-time Maude

Ölveczky, P. C., Boronat, A. & Meseguer, J., Jul 21 2010, Formal Techniques for Distributed Systems - Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010, and 30th IFIP WG 6.1 International Conference, FORTE 2010, Proceedings. p. 47-62 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6117 LNCS).

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

Maude
Formal Semantics
Formal Analysis
Semantics
Real-time

Sequential protocol composition in Maude-NPA

Escobar, S., Meadows, C., Meseguer, J. & Santiago, S., Nov 8 2010, Computer Security, ESORICS 2010 - 15th European Symposium on Research in Computer Security, Proceedings. p. 303-318 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6345 LNCS).

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

Maude
Chemical analysis
Semantics
Operational Semantics
Cryptographic Protocols

The linear temporal logic of rewriting maude model checker

Bae, K. & Meseguer, J., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 208-225 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Maude
Linear Temporal Logic
Temporal logic
Rewriting
Model

Twenty years of rewriting logic

Meseguer, J., Nov 22 2010, Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. p. 15-17 3 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6381 LNCS).

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

Rewriting Logic
Bibliographies
Bibliography
2011

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

Synchronization
Specifications
Automation
Modeling languages

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

Preface

Agha, G. A., Danvy, O. & Meseguer, J., Dec 1 2011, Formal Modeling: Actors, Open Systems, Biological Systems: Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. Vol. 7000 LNCS. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7000 LNCS).

Research output: Chapter in Book/Report/Conference proceedingForeword/postscript

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption

Escobar, S., Kapur, D., Lynch, C., Meadows, C., Meseguer, J., Narendran, P. & Sasse, R., Sep 2 2011, PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming. p. 65-76 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

Homomorphic Encryption
Maude
Unification
Cryptography
Modulo

Protocol analysis modulo combination of theories: A case study in maude-NPA

Sasse, R., Escobar, S., Meadows, C. & Meseguer, J., Oct 19 2011, Security and Trust Management - 6th International Workshop, STM 2010, Revised Selected Papers. p. 163-178 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6710 LNCS).

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

Maude
Unification
Modulo
Network protocols
Equivalence

Proving safety properties of rewrite theories

Rocha, C. & Meseguer, J., Sep 26 2011, Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings. p. 314-328 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6859 LNCS).

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

Concurrent Systems
Safety
Reasoning
Temporal Reasoning
Deductive System

PVeStA: A parallel statistical model checking and quantitative analysis tool

AlTurki, M. & Meseguer, J., Sep 26 2011, Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Proceedings. p. 386-392 7 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6859 LNCS).

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

Model checking
Quantitative Analysis
Model Checking
Statistical Model
Chemical analysis

State/event-based LTL model checking under parametric generalized fairness

Bae, K. & Meseguer, J., Jul 20 2011, Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings. p. 132-148 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6806 LNCS).

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

Model checking
Fairness
Model Checking
Maude
Concurrent Systems

Synchronous AADL and its formal analysis in real-time maude

Bae, K., Ölveczky, P. C., Al-Nayeem, A. & Meseguer, J., Nov 9 2011, Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Proceedings. p. 651-667 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6991 LNCS).

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

Maude
Formal Analysis
Avionics
Synchronous Systems
Real-time

The rewriting logic semantics project: A progress report

Meseguer, J. & Roşu, G., Sep 9 2011, Fundamentals of Computation Theory - 18th International Symposium, FCT 2011, Proceedings. p. 1-37 37 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6914 LNCS).

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

Rewriting Logic
Semantics
Computer hardware
Scalability
Modeling Language

Variants, unification, narrowing, and symbolic reachability in Maude 2.6

Durán, F., Eker, S., Escobar, S., Meseguer, J. & Talcott, C., Dec 1 2011, 22nd International Conference on Rewriting Techniques and Applications, RTA 2011. p. 31-40 10 p. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 10).

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

Substitution reactions
Network protocols
Industry

Verification of microarchitectural refinements in rule-based systems

Dave, N., Katelman, M., King, M., Arvind & Meseguer, J., Sep 1 2011, 9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011. p. 61-71 11 p. 5970511. (9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011).

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

Rule-based Systems
Knowledge based systems
Refinement
Timing
Correctness

Vlogsl: A strategy language for simulation-based verification of hardware

Katelman, M. & Meseguer, J., Mar 30 2011, Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Revised Selected Papers. p. 129-145 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6504 LNCS).

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

Hardware
Surface mount technology
Level control
Simulation
Engineers
2012

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

Linear Temporal Logic
Temporal logic
Rewriting
Maude
Logic

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

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

Quality of service

Folding variant narrowing and optimal variant termination

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

Research output: Contribution to journalArticle

Folding
Termination
Modulo
Unification
Axioms

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

Real time systems
Formalization
Distributed Systems
Correctness
Real-time

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

On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories

Durán, F. & Meseguer, J., Oct 1 2012, In : Journal of Logic and Algebraic Programming. 81, 7-8, p. 816-850 35 p.

Research output: Contribution to journalArticle

Religious buildings
Specifications
Axioms
Temporal logic
Model checking

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

Order-sorted equational unification revisited

Hendrix, J. & Meseguer, J., Dec 20 2012, In : Electronic Notes in Theoretical Computer Science. 290, p. 37-50 14 p.

Research output: Contribution to journalArticle

Unification
Maude
Decision Procedures
Axioms

PALS-based analysis of an airplane multirate control system in real-time maude

Bae, K., Krisiloff, J., Meseguer, J. & Ölveczky, P. C., Dec 29 2012, In : Electronic Proceedings in Theoretical Computer Science, EPTCS. 105, p. 5-21 17 p.

Research output: Contribution to journalConference article

Open Access
Aircraft
Control systems
Hybrid systems
Systems analysis
Distributed parameter control systems

Rewriting semantics of production rule sets

Katelman, M., Keller, S. & Meseguer, J., Oct 1 2012, In : Journal of Logic and Algebraic Programming. 81, 7-8, p. 929-956 28 p.

Research output: Contribution to journalArticle

Production Rules
Rewriting
Semantics
Rewriting Logic
Asynchronous Circuits

Security Policies and Security Models

Goguen, J. A. & Meseguer, J., Jul 6 2012, In : Proceedings - IEEE Symposium on Security and Privacy. 2012-July, July, p. 11-20 10 p., 6234468.

Research output: Contribution to journalConference article

Computer systems

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

Twenty years of rewriting logic

Meseguer, J., Oct 1 2012, In : Journal of Logic and Algebraic Programming. 81, 7-8, p. 721-781 61 p.

Research output: Contribution to journalArticle

Rewriting Logic
Bioinformatics
Semantics
Specifications
Hardware

Unwinding and Inference Control

Goguen, J. A. & Meseguer, J., Jul 6 2012, In : Proceedings - IEEE Symposium on Security and Privacy. 2012-July, July, p. 75-86 12 p., 6234812.

Research output: Contribution to journalConference article

Security of data