Browse Research and Tech Reports - Computer Science by Author "Escobar, Santiago"

  • Cholewa, Andrew; Escobar, Santiago; Meseguer, José (2014-08-29)
    For an unconditional equational theory (Σ,E) whose oriented equations E⃗ are confluent and terminating, narrowing provides an E-unification algorithm. This has been generalized by various authors in two directions: (i) by ...

    application/pdf

    application/pdfPDF (589kB)
  • Escobar, Santiago; Meseguer, José; Sasse, Ralf (2008-04)
    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 Comon-Lundh and Delaune iff for each term t there is a ...

    application/pdf

    application/pdfPDF (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

    application/pdfPDF (443kB)
  • Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José (2011-07-28)
    Generalization, also called anti-unification, 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

    application/pdfPDF (696kB)
  • Yang, Fan; Escobar, Santiago; Meadows, Catherine; Meseguer, José; Santiago, Sonia (2016-07)
    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

    application/pdfPDF (457kB)
  • Escobar, Santiago; Meseguer, José (2007-02)
    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

    application/pdfPDF (373kB)
  • Escobar, Santiago; Meseguer, José; Sasse, Ralf (2007-10)
    Narrowing is a well-known complete procedure for equational E-unification 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

    application/pdfPDF (309kB)
  • Escobar, Santiago; Meseguer, José; Sasse, Ralf (2009-03)
    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

    application/pdfPDF (312kB)
  • Escobar, Santiago; Meseguer, José; Sasse, Ralf (2009-03)
    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

    application/pdfPDF (312kB)
  • Cholewa, Andrew; Meseguer, José; Escobar, Santiago (2014-02-11)
    Variants and the finite variant property were originally introduced about a decade ago by Hurbert Comon-Lundh and Stephanie Delaune to reason about equational theories that commonly appear in cryptographic protocol analysis. ...

    application/pdf

    application/pdfPDF (340kB)