 IDEALS Home
 →
 College of Engineering
 →
 Dept. of Computer Science
 →
 Browse Dept. of Computer Science by Author
Browse Dept. of Computer Science by Author "Escobar, Santiago"
Now showing items 110 of 10

Cholewa, Andrew; Escobar, Santiago; Meseguer, José (20140829)For an unconditional equational theory (Σ,E) whose oriented equations E⃗ are confluent and terminating, narrowing provides an Eunification algorithm. This has been generalized by various authors in two directions: (i) by ...
application/pdf
PDF (589kB) 
Escobar, Santiago; Meseguer, José; Sasse, Ralf (200804)An equational theory decomposed into a set B of equational axioms and a set \Delta of rewrite rules has the \emph{finite variant} (FV) \emph{property} in the sense of ComonLundh and Delaune iff for each term t there is a ...
application/pdf
PDF (468kB) 
Escobar, Santiago; Sasse, Ralf; Meseguer, José (Elsevier, 2012)Automated reasoning modulo an equational theory $\caE$ is a fundamental technique in many applications. If $\caE$ can be split as a disjoint union $E\!\cup \!Ax$ in such a way that $E$ is confluent, terminating, ...
application/pdf
PDF (443kB) 
Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José (20110728)Generalization, also called antiunification, is the dual of unification. Given terms t and t', a generalization is a term t'' of which t and t' are substitution instances. The dual of a most general unifier (mgu) is that ...
application/pdf
PDF (696kB) 
Yang, Fan; Escobar, Santiago; Meadows, Catherine; Meseguer, José; Santiago, Sonia (201607)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 ...
application/pdf
PDF (457kB) 
Escobar, Santiago; Meseguer, José (200702)Rewriting is a general and expressive way of specifying concurrent systems, where concurrent transitions are axiomatized by rewrite rules. Narrowing is a complete symbolic method for model checking reachability properties. ...
application/pdf
PDF (373kB) 
Escobar, Santiago; Meseguer, José; Sasse, Ralf (200710)Narrowing is a wellknown complete procedure for equational Eunification when E can be decomposed as a union E = \Delta \uplus B with B a set of axioms for which a finitary unification algorithm exists, and \Delta a set ...
application/pdf
PDF (309kB) 
Escobar, Santiago; Meseguer, José; Sasse, Ralf (200903)For narrowing with a set of rules \Delta modulo a set of axioms B almost nothing is known about terminating narrowing strategies, and basic narrowing is known to be incomplete for B=AC. In this work we ask and answer the ...
application/pdf
PDF (312kB) 
Escobar, Santiago; Meseguer, José; Sasse, Ralf (200903)For narrowing with a set of rules \Delta modulo a set of axioms B almost nothing is known about terminating narrowing strategies, and basic narrowing is known to be incomplete for B=AC. In this work we ask and answer the ...
application/pdf
PDF (312kB) 
Cholewa, Andrew; Meseguer, José; Escobar, Santiago (20140211)Variants and the finite variant property were originally introduced about a decade ago by Hurbert ComonLundh and Stephanie Delaune to reason about equational theories that commonly appear in cryptographic protocol analysis. ...
application/pdf
PDF (340kB)
Now showing items 110 of 10