Zobrazeno 1 - 10
of 375
pro vyhledávání: '"Meseguer, Jose"'
Autor:
Meseguer, Jose
An inductive inference system for proving validity of formulas in the initial algebra $T_{\mathcal{E}}$ of an order-sorted equational theory $\mathcal{E}$ is presented. It has 20 inference rules, but only 9 of them require user interaction; the remai
Externí odkaz:
http://arxiv.org/abs/2405.02420
Publikováno v:
J. Logic. Algebr. Program 134 (2023) article 100887
Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represente
Externí odkaz:
http://arxiv.org/abs/2402.00275
Publikováno v:
In Developmental and Comparative Immunology January 2025 162
Autor:
Aparicio-Sánchez, Damián, Escobar, Santiago, Meadows, Catherine, Meseguer, Jose, Sapiña, Julia
We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition semantics that takes account o
Externí odkaz:
http://arxiv.org/abs/2010.13707
This paper presents a rewriting logic specification of the Illinois Browser Operating System (IBOS) and defines several security properties, including the same-origin policy (SOP) in reachability logic. It shows how these properties can be deductivel
Externí odkaz:
http://arxiv.org/abs/2005.12232
Autor:
Durán, Francisco, Eker, Steven, Escobar, Santiago, Martí-Oliet, Narciso, Meseguer, José, Rubio, Rubén, Talcott, Carolyn
Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories.
Externí odkaz:
http://arxiv.org/abs/1910.08416
Autor:
Meseguer, José
Publikováno v:
In Journal of Logical and Algebraic Methods in Programming August 2023 134
Publikováno v:
In Journal of Logical and Algebraic Methods in Programming August 2023 134
Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cry
Externí odkaz:
http://arxiv.org/abs/1904.09946
The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-
Externí odkaz:
http://arxiv.org/abs/1808.05097