Ponències/Comunicacions de congressos

Enviaments recents

  • Anotaciones de Merlín, comportamiento de universos y semántica algebraica 

    Nivela Alós, M. Pilar Brígida; Orejas Valdés, Fernando (E.T.S.I. de Telecomunicación, 1985)
    Text en actes de congrés
    Accés obert
    En este trabajo se presentan las ideas básicas seguidas para el diseño de un lenguaje de anotaciones para el lenguaje de programación Merlín. En concreto, las anotaciones se prevén en forma de especificaciones ecuacionales ...

  • 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)
    Text en actes de congrés
    Accés obert
    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 ...

  • Look-ahead with mini-bucket heuristics for MPE 

    Dechter, Rina; Kask, Kalev; Lam, William; Larrosa Bondia, Francisco Javier (AAAI Press (Association for the Advancement of Artificial Intelligence), 2016)
    Comunicació de congrés
    Accés obert
    The paper investigates the potential of look-ahead in the con-text of AND/OR search in graphical models using the Mini-Bucket heuristic for combinatorial optimization tasks (e.g., MAP/MPE or weighted CSPs). We present and ...

  • Limited discrepancy AND/OR search and its application to optimization tasks in graphical models 

    Larrosa Bondia, Francisco Javier; Rollón Rico, Emma; Dechter, Rina (AAAI Press (Association for the Advancement of Artificial Intelligence), 2016)
    Text en actes de congrés
    Accés obert
    Many combinatorial problems are solved with a Depth-First search (DFS) guided by a heuristic and it is well-known that this method is very fragile with respect to heuristic mistakes. One standard way to make DFS more robust ...

  • Compositional safety verification with Max-SMT 

    Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2015)
    Text en actes de congrés
    Accés obert
    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)
    Text en actes de congrés
    Accés obert
    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)
    Text en actes de congrés
    Accés restringit per política de l'editorial
    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)
    Text en actes de congrés
    Accés obert
    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)
    Text en actes de congrés
    Accés obert
    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)
    Text en actes de congrés
    Accés obert
    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)
    Text en actes de congrés
    Accés obert
    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)
    Text en actes de congrés
    Accés restringit per política de l'editorial
    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 ...

Mostra'n més