Now showing items 1-20 of 20

    • A Fully syntactic AC-RPO 

      Rubio Gimeno, Alberto (1998-02-01)
      External research report
      Open Access
      We present the first fully syntactic (i.e., non-interpretation-based) AC-compatible recursive path ordering (RPO). It is very simple, and hence easy to implement, and its behaviour is intuitive as in the standard RPO. ...
    • Basic superposition is complete 

      Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
      External research report
      Open Access
      We define a formalism of equality constraints and use it to prove the completeness of what we have called basic superposition: a restricted form of superposition in which only the subterms not originated in previous ...
    • Compositional safety verification with Max-SMT 

      Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2015)
      Conference report
      Open Access
      We present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop) and a postcondition, we show how to, using ...
    • Disseny i implantació de les assignatures de programació als nous Graus d'enginyeria informàtica 

      Rubio Gimeno, Alberto (Universitat Politècnica de Catalunya. Institut de Ciències de l'Educació, 2012-02-07)
      Conference lecture / Conference report
      Open Access
    • Extension orderings 

      Rubio Gimeno, Alberto (1995-10)
      External research report
      Open Access
      In this paper we study how to extend a collection of term orderings on disjoint signatures to a single one, called an extension ordering, which preserves (part of) their properties. Apart of its own interest, e.g. in ...
    • First-order completion with ordering constraints: some positive and some negative results 

      Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
      External research report
      Open Access
      We show by means of counter examples that some well-known results on the completeness of deduction methods with ordering constraints are incorrect. The problem is caused by the fact that the usual lifting lemmata do not ...
    • Higher-order recursive path orderings 

      Jouannaud, J P; Rubio Gimeno, Alberto (1998-12)
      External research report
      Open Access
      This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to higher-order simply-typed lambda-terms. The main result ...
    • 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 ...
    • Jutge.org: characteristics and experiences 

      Petit Silvestre, Jordi; Roura Ferret, Salvador; Carmona Vargas, Josep; Cortadella, Jordi; Duch Brown, Amalia; Giménez, Omer; Mani, Anaga; Mas Rovira, Jan; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto; San Pedro Martín, Javier de; Venkataramani, Divya (2018-07)
      Article
      Open Access
      Jutge.org is an open educational online programming judge designed for students and instructors, featuring a repository of problems that is well organized by courses, topics and difficulty. Internally, Jutge.org uses a ...
    • Lambda extensions of rewrite orderings 

      Jouannaud, Jean Pierre; Rubio Gimeno, Alberto (1995-10)
      External research report
      Open Access
      In this work we provide a new proof of the result by Gallier and Tannen that the combination of an arbitrary terminating first-order rewrite system with the simply typed lambda calculus is strongly normalizing. This proof ...
    • Minimal-model-guided approaches to solving polynomial constraints and extensions 

      Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2014)
      Conference report
      Open Access
      In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear ...
    • Nominal completion for rewrite systems with binders 

      Fernández, Maribel; Rubio Gimeno, Alberto (Springer, 2012)
      Conference report
      Restricted access - publisher's policy
      We design a completion procedure for nominal rewriting systems, based on a generalisation of the recursive path ordering to take into account alpha equivalence. Nominal rewriting generalises first-order rewriting by providing ...
    • Normal higher-order termination 

      Jouannaud, Jean Pierre; Rubio Gimeno, Alberto (2015-03-01)
      Article
      Open Access
      We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of ...
    • 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 non-termination using max-SMT 

      Larraz Hurtado, Daniel; Nimkar, Kaustubh; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2014)
      Conference report
      Open Access
      We show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants - properties such ...
    • Proving termination of imperative programs using Max-SMT 

      Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2013)
      Conference report
      Open Access
      We show how Max-SMT can be exploited in constraint-based program termination proving. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different ...
    • 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 ...
    • Speeding up the constraint-based method in difference logic 

      Candeago, L.; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2016)
      Conference report
      Open Access
      Over the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of ...
    • Termination competition (termCOMP 2015) 

      Giesl, Jürgen; Mesnard, Frédéric; Rubio Gimeno, Alberto; Thiemann, René; Waldmann, Johannes (Springer, 2015)
      Conference report
      Open Access
      The termination competition focuses on automated termination analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. ...
    • The computability path ordering 

      Blanqui, Frédéric; Jouannaud, Jean Pierre; Rubio Gimeno, Alberto (2015-10-26)
      Article
      Open Access
      This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation ...