Ponències/Comunicacions de congressos: Enviaments recents

Ara es mostren els items 1-12 de 30

    • Choosing the root of the tree decomposition when solving WCSPs: preliminary results 

      Petrova, Aleksandra; Larrosa Bondia, Francisco Javier; Rollón Rico, Emma (IOS Press, 2021)
      Text en actes de congrés
      Accés obert
      In this paper we analyze the effect of selecting the root in a tree decomposition when using decomposition-based backtracking algorithms. We focus on optimization tasks for Graphical Models using the BTD algorithm. We show ...

    • Stuck-at-off fault analysis in memristor-based architecture for synchronization 

      Escudero, Manuel; Vourkas, Ioannis; Rubio Gimeno, Alberto (Institute of Electrical and Electronics Engineers (IEEE), 2019)
      Text en actes de congrés
      Accés restringit per política de l'editorial
      Nonlinear circuits may be interconnected and organized in networks to couple their dynamics and achieve synchronization, a process that is commonly observed in nature. Recent works have shown that memristors may be used ...

    • Decision levels are stable: towards better SAT heuristics 

      Nieuwenhuis, Robert Lukas Mario; Lozano Navarro, Adrián; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (EasyChair Publications, 2020)
      Text en actes de congrés
      Accés restringit per política de l'editorial
      We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals ...

    • Augmenting the power of (partial) MaxSat resolution with extension 

      Larrosa Bondia, Francisco Javier; Rollón Rico, Emma (AAAI Press, 2020)
      Comunicació de congrés
      Accés restringit per política de l'editorial
      The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof ...

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

    • Ordocoordinación: cómo organizar 700 estudiantes en un nuevo campus (y no morir en el intento) 

      Castro Rabal, Jorge; Farreres de la Morena, Xavier; Gabarró Vallès, Joaquim; Nivela Alós, M. Pilar Brígida; Pérez Poch, Antoni; Pino Blanco, Elvira; Rivero Almeida, José Miguel (Asociación de Enseñantes Universitarios de la Informática (AENUI), 2018)
      Text en actes de congrés
      Accés obert
      Since Autumn Term 2017 the Department of Computer Science of the Universitat Politecnica de Catalunya UPC-BarcelonaTech is in charge of teaching ”Fundamentals of Programming” in the new DiagonalBeso ´s Campus, at EEBE ...

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