Now showing items 1-18 of 18

    • A parametric approach for smaller and better encodings of cardinality constraints 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2013)
      Conference report
      Open Access
      Adequate encodings for high-level constraints are a key ingredient for the application of SAT technology. In particular, cardinality constraints state that at most (at least, or exactly) k out of n propositional variables ...
    • Automatic generation of polynomial loop invariants: algebraic foundations 

      Rodríguez Carbonell, Enric; Kapur, Dikkar (2004-01)
      External research report
      Open Access
      A general framework is presented for automating the discovery of loop invariants for imperative programs. Theoretical results about the correctness and completeness of the proposed method are given. More importantly, it ...
    • BDDs for Pseudo-Boolean Constraints 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer Verlag, 2011)
      Conference report
      Restricted access - publisher's policy
      Pseudo-Boolean constraints are omnipresent in practical applications, and therefore a significant effort has been devoted to the development of good SAT encoding techniques for these constraints. Several of these encodings ...
    • Cardinality networks and their applications 

      Asín Acha, Roberto Javier; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2009)
      Conference report
      Restricted access - publisher's policy
      We introduce Cardinality Networks, a new CNF encoding of cardinality constraints. It improves upon the previously existing encodings such as the sorting networks of [ES06] in that it requires much less clauses and auxiliary ...
    • 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 ...
    • 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)
      Conference report
      Restricted access - publisher's policy
      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 ...
    • Estructures de Dades i Algorismes Col·lecció d’Exàmens 

      Duch Brown, Amalia; Rodríguez Carbonell, Enric (Universitat Politècnica de Catalunya, 2011-09-09)
      Exam
      Restricted access to the UPC academic community
    • Generation of basic semi-algebraic invariants using convex polyhedra 

      Bagnara, Roberto; Rodríguez Carbonell, Enric; Zaffanella, Enea (2005-04)
      External research report
      Open Access
      A technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation framework. It is based on overapproximating basic semi-algebraic sets, i.e., sets defined ...
    • Incomplete SMT techniques for solving non-linear formulas over the integers 

      Borralleras Andreu, Cristina; Larraz Hurtado, Daniel; Rodríguez Carbonell, Enric; Oliveras Llunell, Albert; Rubio Gimeno, Alberto (2019-08-01)
      Article
      Open Access
      We present new methods for solving the Satisfiability Modulo Theories problem over the theory of QuantifierFree Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of deciding the satisfiability of ground formulas ...
    • Joc d’estructures de dades i algorismes 

      Duch Brown, Amalia; Petit Silvestre, Jordi; Rodríguez Carbonell, Enric; Roura Ferret, Salvador (Universitat Politècnica de Catalunya. Institut de Ciències de l'Educació, 2014-04-24)
      Conference report
      Open Access
      L'activitat consisteix en la implementació d'un jugador per a un joc d'ordinador. L'objectiu és que els estudiants hi apliquin els algorismes i estructures de dades explicats en el curs. Un joc consisteix en un tauler on ...
    • Jutge.org: characteristics and experiences 

      Petit Silvestre, Jordi; Roura Ferret, Salvador; Carmona Vargas, Josep; Cortadella, Jordi; Duch Brown, Amalia; Giménez, Omer; Mani, Anaga; Mas Rovira, Jan; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto; San Pedro Martín, Javier de; Venkataramani, Divya (2018-07)
      Article
      Open Access
      Jutge.org is an open educational online programming judge designed for students and instructors, featuring a repository of problems that is well organized by courses, topics and difficulty. Internally, Jutge.org uses a ...
    • 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 ...
    • On schema and functional architectures for multilevel secure and multiuser model federated DB systems 

      Rodríguez Carbonell, Enric; Oliva, M.; Saltor Soler, Félix Enrique; Campderrich, B. (1997-07-02)
      External research report
      Open Access
      This paper presents an approach for tightly federated database systems with several federated schemas that consists of a schema architecture and a functional architecture. The reference schema architecture has been ...
    • 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 ...
    • Proving termination of imperative programs using Max-SMT 

      Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2013)
      Conference report
      Open Access
      We show how Max-SMT can be exploited in constraint-based program termination proving. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different ...
    • 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)
      Conference report
      Open Access
      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 ...
    • 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)
      Conference report
      Open Access
      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 ...
    • To encode or to propagate? The best choice for each constraint in SAT 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Stuckey, Peter (Springer, 2013)
      Conference report
      Open Access
      Sophisticated compact SAT encodings exist for many types of constraints. Alternatively, for instances with many (or large) constraints, the SAT solver can also be extended with built-in propagators (the SAT Modulo Theories ...