Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014-11)
The notion of *operational termination* captures nonterminating computations due to subsidiary processes that are necessary to issue a *single* `main' step but which often remain `hidden' when the main computation sequence ...
The development of powerful techniques for proving termination of rewriting modulo a set of equational axioms is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, ELAN, OBJ, etc. ...
Generalization, also called anti-unification, is the dual of unification. Given terms t and t
,
a generalizer is a term t of which t and t are substitution instances. The dual of
a most general unifier (mgu) is that of ...
[EN] Partial evaluation is a powerful and general program optimization technique with many successful applications. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ...
Computing generalizers is relevant in a wide spectrum of automated
reasoning areas where analogical reasoning and inductive inference
are needed. The ACUOS system computes a complete and minimal
set of semantic generalizers ...
Computing generalizers is relevant in a wide spectrum of automated
reasoning areas where analogical reasoning and inductive inference
are needed. The ACUOS system computes a complete and minimal
set of semantic generalizers ...
Erbatur, Serdar; Escobar Román, Santiago; Kapur, Deepak; Liu, Zhiqiang; Lynch, Christopher A.; Meadows, Catherine; Meseguer, José; Narendran, Paliath; Santiago Pinazo, Sonia; Sasse, Ralf(Springer, 2013)
We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition ...
Lucas Alba, Salvador; Meseguer, José(Elsevier, 2017-01)
[EN] The notion of operational termination provides a logic-based definition of termination of computational systems as the absence of infinite inferences in the computational logic describing the operational semantics of ...
We address a problem that arises in cryptographic protocol
analysis when the equational properties of the cryptosystem are taken
into account: in many situations it is necessary to guarantee that certain
terms generated ...
Escobar Román, Santiago; Sasse, Ralf; Meseguer, José(Elsevier, 2012-11)
Automated reasoning modulo an equational theory E is a fundamental technique in many applications. If E can be split as a disjoint union E u Ax in such a way that E is confluent, terminating, sort-decreasing, and coherent ...
Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014)
Reasoning about termination of declarative programs, which are described by means of a computational logic, requires the definition of appropriate abstractions as semantic models of the logic, and also handling the conditional ...
[EN] Generalization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t' is a term t '' of which t and t' are substitution instances. The dual of most general equational unifiers ...
[EN] 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 ...
There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic ...
[EN] 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 ...
Lucas Alba, Salvador; Meseguer, José(ACM, 2014-09)
A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) ...
Escobar Román, Santiago; Meadows, Cahterine; Meseguer, José; Santiago Pinazo, Sonia(Elsevier, 2014-11)
The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and ...
Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014-11)
This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems ...
Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl(Elsevier, 2018-09)
[EN] Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite ...
Lucas Alba, Salvador; Meseguer, José; Gutiérrez Gil, Raúl(Springer-Verlag, 2020-10)
[EN] Proving termination of programs in `real-life¿ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully cap- turing the impact in the termination ...