González Burgueño, Antonio; Santiago Pinazo, Sonia; Escobar Román, Santiago; Meadows, Catherine; Meseguer, Jose(Springer International Publishing, 2014)
Standards for cryptographic protocols have long been attractive
candidates for formal verification. It is important that such standards
be correct, and cryptographic protocols are tricky to design and subject
to ...
Cholewa, Andrew; Escobar Román, Santiago; Meseguer, Jose(Elsevier, 2015-11)
For an unconditional equational theory (Sigma, E) whose oriented equations (E) over arrow are confluent and terminating, narrowing provides an E-unification algorithm. This has been generalized by various authors in two ...
Lucas Alba, Salvador; Meseguer, Jose(Elsevier, 2016-01)
We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the ...
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 ...