Program Verification Using Automatic Generation of Invariants. - Enric Rodríguez-Carbonell; Deepak Kapur (ICTAC, 2004)

Automatic generation of polynomial loop. - Enric Rodríguez-Carbonell; Deepak Kapur (ISSAC, 2004)

An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants. - Enric Rodríguez-Carbonell; Deepak Kapur (SAS, 2004)

Derivation of Non-structural Invariants of Petri Nets Using Abstract Interpretation. - Robert Clarisó; Enric Rodríguez-Carbonell; Jordi Cortadella (ICATPN, 2005)

Generating Polynomial Invariants for Hybrid Systems. - Enric Rodríguez-Carbonell; Ashish Tiwari 001 (HSCC, 2005)

Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra. - Roberto Bagnara; Enric Rodríguez-Carbonell; Enea Zaffanella (SAS, 2005)

Challenges in Satisfiability Modulo Theories. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (RTA, 2007)

Generating all polynomial invariants in simple loops. - Enric Rodríguez-Carbonell; Deepak Kapur (J. Symb. Comput., 2007)

Automatic generation of polynomial invariants of bounded degree using abstract interpretation. - Enric Rodríguez-Carbonell; Deepak Kapur (Sci. Comput. Program., 2007)

The Barcelogic SMT Solver. - Miquel Bofill; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (CAV, 2008)

A Write-Based Solver for SAT Modulo the Theory of Arrays. - Miquel Bofill; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (FMCAD, 2008)

Efficient Generation of Unsatisfiability Proofs and Cores in SAT. - Roberto Asín; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (LPAR, 2008)

The Max-Atom Problem and Its Relevance. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (LPAR, 2008)

SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. - Germain Faure; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2008)

Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (Discret. Appl. Math., 2008)

Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. - Cristina Borralleras; Salvador Lucas; Rafael Navarro-Marset; Enric Rodríguez-Carbonell; Albert Rubio (CADE, 2009)

Cardinality Networks and Their Applications. - Roberto Asín; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2009)

Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. - Javier Larrosa; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2009)

Semiring-Induced Propositional Logic: Definition and Basic Algorithms. - Javier Larrosa; Albert Oliveras; Enric Rodríguez-Carbonell (LPAR (Dakar), 2010)

Practical algorithms for unsatisfiability proof and core generation in SAT solvers. - Roberto Javier Asín Achá; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (AI Commun., 2010)

Preface. - Antoine Miné; Enric Rodríguez-Carbonell (NSAD@SAS, 2010)

Hard problems in max-algebra, control theory, hypergraphs and other areas. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (Inf. Process. Lett., 2010)

BDDs for Pseudo-Boolean Constraints - Revisited. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2011)

Cardinality Networks: a theoretical and empirical study. - Roberto Asín; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (Constraints An Int. J., 2011)

A Framework for Certified Boolean Branch-and-Bound Optimization. - Javier Larrosa; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (J. Autom. Reason., 2011)

A New Look at BDDs for Pseudo-Boolean Constraints. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Valentin Mayer-Eichberger (J. Artif. Intell. Res., 2012)

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. - Cristina Borralleras; Salvador Lucas; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (J. Autom. Reason., 2012)

A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (CP, 2013)

To Encode or to Propagate? The Best Choice for Each Constraint in SAT. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Peter J. Stuckey (CP, 2013)

Fun in CS2. - Amalia Duch; Jordi Petit; Enric Rodríguez-Carbonell; Salvador Roura (CSEDU, 2013)

Proving termination of imperative programs using Max-SMT. - Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (FMCAD, 2013)

SMT-Based Array Invariant Generation. - Daniel Larraz; Enric Rodríguez-Carbonell; Albert Rubio (VMCAI, 2013)

The recursive path and polynomial ordering for first-order and higher-order terms. - Miquel Bofill; Cristina Borralleras; Enric Rodríguez-Carbonell; Albert Rubio (J. Log. Comput., 2013)

Proving Non-termination Using Max-SMT. - Daniel Larraz; Kaustubh Nimkar; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (CAV, 2014)

Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. - Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (SAT, 2014)

Compositional Safety Verification with Max-SMT. - Marc Brockschmidt; Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (FMCAD, 2015)

Speeding up the Constraint-Based Method in Difference Logic. - Lorenzo Candeago; Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (SAT, 2016)

Proving Termination Through Conditional Termination. - Cristina Borralleras; Marc Brockschmidt; Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (TACAS (1), 2017)

Jutge.org: Characteristics and Experiences. - Jordi Petit; Salvador Roura; Josep Carmona 001; Jordi Cortadella; Jordi Duch; Omer Giménez; Anaga Mani; Jan Mas; Enric Rodríguez-Carbonell; Enric Rubio; Enric de San Pedro; Divya Venkataramani (IEEE Trans. Learn. Technol., 2018)

Corrections to "Jutge.org: Characteristics and Experiences". - Jordi Petit; Salvador Roura; Josep Carmona 001; Jordi Cortadella; Jordi Duch; Omer Giménez; Anaga Mani; Jan Mas; Enric Rodríguez-Carbonell; Enric Rubio; Enric de San Pedro; Divya Venkataramani (IEEE Trans. Learn. Technol., 2019)

Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. - Cristina Borralleras; Daniel Larraz; Enric Rodríguez-Carbonell; Albert Oliveras; Albert Rubio (ACM Trans. Comput. Log., 2019)

Decision levels are stable: towards better SAT heuristics. - Robert Nieuwenhuis; Adrià Lozano; Albert Oliveras; Enric Rodríguez-Carbonell (LPAR, 2020)

A Heuristic Approach to the Design of Optimal Cross-Docking Boxes. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (IEEE Access, 2021)

Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Emma Rollon (IEEE Access, 2021)

Analyzing Multiple Conflicts in SAT: An Experimental Evaluation. - Albert Oliveras; Enric Rodríguez-Carbonell; Rui Zhao (LPAR, 2023)

Speeding up Pseudo-Boolean Propagation. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Rui Zhao (SAT, 2024)

IntSat: integer linear programming by conflict-driven constraint learning. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (Optim. Methods Softw., 2024)

Symbolic Conflict Analysis in Pseudo-Boolean Optimization. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Rui Zhao (SAT, 2025)