Recent Submissions

  • 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 ...
  • 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 ...

View more