Recent Submissions

  • Resolvedor SAT, basado en procedimientos Davis-Putnam-Longemann-Loveland 

    Gabriel Cerna, Pedro Víctor; Nieuwenhuis, Robert Lukas Mario (2007-01)
    External research report
    Open Access
    El problema de satisfación de fórmulas lógicas (SAT), es un problema NP-Hard. Una forma de resolverlo es por medio de procedimientos Davis-Putnam-Longemann-Loveland (DPLL), ahora presentamos una implementación de un ...
  • 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 ...
  • Termination competition (termCOMP 2015) 

    Giesl, Jürgen; Mesnard, Frédéric; Rubio Gimeno, Alberto; Thiemann, René; Waldmann, Johannes (Springer, 2015)
    Conference report
    Restricted access - publisher's policy
    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 ...
  • Exponential separation between tree-like and dag-like Cutting Planes proof systems 

    Bonet Carbonell, M. Luisa; Esteban Ángeles, Juan Luis; Galesi, Nicola; Johannsen, Jan (1997-12)
    External research report
    Open Access
    We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like ...
  • 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 ...
  • The fractal dimension of SAT formulas 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Giráldez Crú, Jesús; Levy Diaz, Jordi (Springer, 2014)
    Conference report
    Restricted access - publisher's policy
    Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit ...
  • Decomposing utility functions in Bounded Max-Sum for distributed constraint optimization 

    Rollón Rico, Emma; Larrosa Bondia, Francisco Javier (Springer, 2014)
    Conference report
    Open Access
    Bounded Max-Sum is a message-passing algorithm for solving distributed Constraint Optimization Problems (DCOP) able to compute solutions with a guaranteed approximation ratio. In this paper we show that the introduction ...
  • The IntSat method for integer linear programming 

    Nieuwenhuis, Robert Lukas Mario (Springer, 2014)
    Conference report
    Open Access
    Conflict-Driven Clause-Learning (CDCL) SAT solvers can automatically solve very large real-world problems. To go beyond, and in particular in order to solve and optimize problems involving linear arithmetic constraints, ...
  • 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 ...

View more