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
    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 fractal dimension of SAT formulas 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Giráldez Crú, Jesús; Levy Díaz, 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 ...
  • 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 ...
  • Semiring-based mini-bucket partitioning schemes 

    Rollón Rico, Emma; Larrosa Bondia, Francisco Javier; Dechter, Rina (AAAI Press. Association for the Advancement of Artificial Intelligence, 2013)
    Conference report
    Restricted access - publisher's policy
    Graphical models are one of the most prominent frameworks to model complex systems and efficiently query them. Their underlying algebraic properties are captured by a valuation structure that, most usually, is a semiring. ...
  • Improving WPM2 for (weighted) partial MaxSAT 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Gabàs, Joel; Levy Díaz, Jordi (Springer, 2013)
    Conference report
    Restricted access - publisher's policy
    Weighted Partial MaxSAT (WPMS) is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into WPMS. In this paper we extend the state-of-the-art WPM2 ...

View more