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

Research Output 1975 2019

Filter
Article
2018

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

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

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
2015

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

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

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

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

Real time systems
Ailerons
Control systems
Avionics
Clocks
Formal Specification
Fault tolerance
Fault Tolerance
Fault
Masking
Linear Temporal Logic
Temporal logic
Model checking
Rewriting
Model Checking
Surface mount technology
Open systems
Open Systems
Rewriting
Systems Analysis

State space reduction in the Maude-NRL Protocol Analyzer

Escobar, S., Meadows, C., Meseguer, J. & Santiago, S., Jan 1 2014, In : Information and Computation. 238, p. 157-186 30 p.

Research output: Contribution to journalArticle

Maude
Cryptography
State Space
Attack
Completeness
Termination
Algebra
Semantics
Rewriting
Normal Form

Taming distributed system complexity through formal patterns

Meseguer, J., Apr 1 2014, In : Science of Computer Programming. 83, p. 3-34 32 p.

Research output: Contribution to journalArticle

Real time systems
Semantics
2013

The rewriting logic semantics project: A progress report

Meseguer, J. & Rosu, G., Oct 10 2013, In : Information and Computation. 231, p. 38-69 32 p.

Research output: Contribution to journalArticle

Rewriting Logic
Semantics
Computer hardware
Scalability
Modeling Language
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

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

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

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

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 journalArticle

Security of data
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
2010

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

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
2009

A Graphical User Interface for Maude-NPA

Santiago, S., Talcott, C., Escobar, S., Meadows, C. & Meseguer, J., Dec 25 2009, In : Electronic Notes in Theoretical Computer Science. 258, 1, p. 3-20 18 p.

Research output: Contribution to journalArticle

Maude
Graphical User Interface
Graphical user interfaces
Cryptography
Search Trees

A Rewriting Semantics for Maude Strategies

Martí-Oliet, N., Meseguer, J. & Verdejo, A., Jun 29 2009, In : Electronic Notes in Theoretical Computer Science. 238, 3, p. 227-247 21 p.

Research output: Contribution to journalArticle

Maude
Rewriting
Semantics
Requirements
Nondeterminism

Methods for Proving Termination of Rewriting-based Programming Languages by Transformation

Durán, F., Lucas, S. & Meseguer, J., Aug 5 2009, In : Electronic Notes in Theoretical Computer Science. 248, p. 93-113 21 p.

Research output: Contribution to journalArticle

Rewriting
Termination
Computer programming languages
Programming Languages
Axioms

Operational Termination of Membership Equational Programs: the Order-Sorted Way

Lucas, S. & Meseguer, J., Jun 29 2009, In : Electronic Notes in Theoretical Computer Science. 238, 3, p. 207-225 19 p.

Research output: Contribution to journalArticle

Termination
Equational Logic
Rewriting
Logic Programs
Axioms

Order-Sorted Generalization

Alpuente, M., Escobar, S., Meseguer, J. & Ojeda, P., Aug 3 2009, In : Electronic Notes in Theoretical Computer Science. 246, p. 27-38 12 p.

Research output: Contribution to journalArticle

Theorem proving
Polymorphism
Substitution reactions
Unification
Program Synthesis

Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol

AlTurki, M., Meseguer, J. & Gunter, C., Mar 28 2009, In : Electronic Notes in Theoretical Computer Science. 234, C, p. 3-18 16 p.

Research output: Contribution to journalArticle

Protocol Verification
Probabilistic Modeling
Probabilistic Analysis
Network protocols
Bandwidth

Variant Narrowing and Equational Unification

Escobar, S., Meseguer, J. & Sasse, R., Jun 29 2009, In : Electronic Notes in Theoretical Computer Science. 238, 3, p. 103-119 17 p.

Research output: Contribution to journalArticle

Unification
Modulo
Union
Symbolic Analysis
Reachability Analysis

Web Services and Interoperability for the Maude Termination Tool

Durán, F., Lucas, S., Meseguer, J. & Gutiérrez, F., Aug 5 2009, In : Electronic Notes in Theoretical Computer Science. 248, p. 83-92 10 p.

Research output: Contribution to journalArticle

Maude
Interoperability
Termination
Web services
Web Services
2008

Algebraic Stuttering Simulations

Martí-Oliet, N., Meseguer, J. & Palomino, M., Apr 8 2008, In : Electronic Notes in Theoretical Computer Science. 206, C, p. 91-110 20 p.

Research output: Contribution to journalArticle

Rewriting Logic
Simulation
Representability
Categorical
Range of data