Now showing items 1-3 of 3

    • Incomplete SMT techniques for solving non-linear formulas over the integers 

      Borralleras Andreu, Cristina; Larraz Hurtado, Daniel; Rodríguez Carbonell, Enric; Oliveras Llunell, Albert; Rubio Gimeno, Alberto (2019-08-01)
      Article
      Open Access
      We present new methods for solving the Satisfiability Modulo Theories problem over the theory of QuantifierFree Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of deciding the satisfiability of ground formulas ...
    • Path orderings, quasi-orderings and termination of term rewriting systems 

      Borralleras Andreu, Cristina; Rubio Gimeno, Alberto (1997-10)
      External research report
      Open Access
      In this paper we present some original variations of the recursive path ordering. Additionally we define a restricted semantic path ordering which, in general, does not include the subterm relation, but is shown to ...
    • Proving termination through conditional termination 

      Borralleras Andreu, Cristina; Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2017)
      Conference report
      Open Access
      We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine ...