[EN] Maude-NPA is an analysis tool for cryptographic security protocols that takes into account the algebraic properties of the cryptosystem. Maude-NPA can reason about a wide range of cryptographic properties. However, ...

[EN] In the realm of term rewriting, given terms s and t, a reachability condition s>>t is called feasible if there is a substitution O such that O(s) rewrites into O(t) in zero or more steps; otherwise, it is ...

[EN] Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although a good number of techniques for proving termination of context-sensitive rewriting (CSR) have been ...

Context-sensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions ...

[EN] Context-sensitive dependence pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from ...

[EN] Given a Conditional Term Rewriting System (CTRS) R and terms s and t, we say that the reachability condition s ->* t is *feasible* if there is a substitution \sigma instantiating the variables in s and t such that ...

[ES] Las tecnologías de la información y la comunicación dan forma a los sistemas del mundo de hoy, y esos sistemas dan forma a la sociedad en la que vivimos. La seguridad de esos sistemas se basa en problemas matemáticos ...

Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications ...

[EN] MU-TERM is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted ...