Now showing items 1-14 of 14

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