TRIP: An Implementation of Clausal Rewriting. - Robert Nieuwenhuis; Fernando Orejas; Albert Rubio (CADE, 1990)

Theorem Proving with Ordering Constrained Clauses. - Robert Nieuwenhuis; Albert Rubio (CADE, 1992)

Basic Superposition is Complete. - Robert Nieuwenhuis; Albert Rubio (ESOP, 1992)

A Precedence-Based Total AC-Compatible Ordering. - Albert Rubio; Robert Nieuwenhuis (RTA, 1993)

AC-Superposition with Constraints: No AC-Unifiers Needed. - Robert Nieuwenhuis; Albert Rubio (CADE, 1994)

Theorem Proving modulo Associativity. - Albert Rubio (CSL, 1995)

Extension Orderings. - Albert Rubio (ICALP, 1995)

Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) - Hubert Comon; Robert Nieuwenhuis; Albert Rubio (LICS, 1995)

Theorem Proving with Ordering and Equality Constrained Clauses. - Robert Nieuwenhuis; Albert Rubio (J. Symb. Comput., 1995)

A Total AC-Compatible Ordering Based on RPO. - Albert Rubio; Robert Nieuwenhuis (Theor. Comput. Sci., 1995)

A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form. - Jean-Pierre Jouannaud; Albert Rubio (RTA, 1996)

Paramodulation with Built-in AC-Theories and Symbolic Constraints. - Robert Nieuwenhuis; Albert Rubio (J. Symb. Comput., 1997)

Rewrite Orderings for Higher-Order Terms in eta-Long beta-Normal Form and Recursive Path Ordering. - Jean-Pierre Jouannaud; Albert Rubio (Theor. Comput. Sci., 1998)

Paramodulation with Non-Monotonic Orderings. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (LICS, 1999)

The Higher-Order Recursive Path Ordering. - Jean-Pierre Jouannaud; Albert Rubio (LICS, 1999)

Complete Monotonic Semantic Path Orderings. - Cristina Borralleras; Maria Ferreira; Albert Rubio (CADE, 2000)

Modular Redundancy for Theorem Proving. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (FroCoS, 2000)

Paramodulation-Based Theorem Proving. - Robert Nieuwenhuis; Albert Rubio (Handbook of Automated Reasoning, 2001)

A Monotonic Higher-Order Semantic Path Ordering. - Cristina Borralleras; Albert Rubio (LPAR, 2001)

Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. - Miquel Bofill; Albert Rubio (CADE, 2002)

Recursive Path Orderings Can Be Context-Sensitive. - Cristina Borralleras; Salvador Lucas; Albert Rubio (CADE, 2002)

A Fully Syntactic AC-RPO. - Albert Rubio (Inf. Comput., 2002)

Monotonic AC-Compatible Semantic Path Orderings. - Cristina Borralleras; Albert Rubio (RTA, 2003)

Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (J. Autom. Reason., 2003)

Redundancy Notions for Paramodulation with Non-monotonic Orderings. - Miquel Bofill; Albert Rubio (IJCAR, 2004)

Recursive Path Orderings Can Also Be Incremental. - Mirtha-Lina Fernández; Guillem Godoy; Albert Rubio (LPAR, 2005)

Orderings for Innermost Termination. - Mirtha-Lina Fernández; Guillem Godoy; Albert Rubio (RTA, 2005)

Higher-Order Termination: From Kruskal to Computability. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (LPAR, 2006)

Higher-Order Orderings for Normal Rewriting. - Jean-Pierre Jouannaud; Albert Rubio (RTA, 2006)

Orderings and Constraints: Theory and Practice of Proving Termination. - Cristina Borralleras; Albert Rubio (Rewriting, Computation and Proof, 2007)

HORPO with Computability Closure: A Reconstruction. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (LPAR, 2007)

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

Polymorphic higher-order recursive path orderings. - Jean-Pierre Jouannaud; Albert Rubio (J. ACM, 2007)

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

The Computability Path Ordering: The End of a Quest. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (CSL, 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)

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)

Paramodulation with Well-founded Orderings. - Miquel Bofill; Albert Rubio (J. Log. Comput., 2009)

Nominal Completion for Rewrite Systems with Binders. - Maribel Fernández; Albert Rubio (ICALP (2), 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)

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)

Paramodulation with Non-Monotonic Orderings and Simplification. - Miquel Bofill; Albert Rubio (J. Autom. Reason., 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)

Termination Competition (termCOMP 2015). - Jürgen Giesl; Frédéric Mesnard; Albert Rubio; René Thiemann; Johannes Waldmann (CADE, 2015)

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

The computability path ordering. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (Log. Methods Comput. Sci., 2015)

Normal Higher-Order Termination. - Jean-Pierre Jouannaud; Albert Rubio (ACM Trans. Comput. Log., 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)

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. - Elvira Albert; Pablo Gordillo; Benjamin Livshits; Albert Rubio; Ilya Sergey (ATVA, 2018)

Constrained Dynamic Partial Order Reduction. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel; Albert Rubio (CAV (2), 2018)

SDN-Actors: Modeling and Verification of SDN Programs. - Elvira Albert; Miguel Gómez-Zamalloa; Albert Rubio; Matteo Sammartino; Alexandra Silva 001 (FM, 2018)

GASTAP: A Gas Analyzer for Smart Contracts. - Elvira Albert; Pablo Gordillo; Albert Rubio; Ilya Sergey (CoRR, 2018)

SAFEVM: a safety verifier for Ethereum smart contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (ISSTA, 2019)

The Termination and Complexity Competition. - Jürgen Giesl; Albert Rubio; Christian Sternagel; Johannes Waldmann; Akihisa Yamada 002 (TACAS (3), 2019)

Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. - Elvira Albert; Pablo Gordillo; Albert Rubio; Ilya Sergey (VECoS, 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)

Resource Analysis driven by (Conditional) Termination Proofs. - Elvira Albert; Miquel Bofill; Cristina Borralleras; Enrique Martin-Martin; Albert Rubio (Theory Pract. Log. Program., 2019)

Synthesis of Super-Optimized Smart Contracts Using Max-SMT. - Elvira Albert; Pablo Gordillo; Albert Rubio; Maria Anna Schett (CAV (1), 2020)

Smart, and also Reliable and Gas-Efficient, Contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (ICST, 2020)

GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (TACAS (2), 2020)

Actor-Based Model Checking for SDN Networks. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel; Albert Rubio; Matteo Sammartino; Alexandra Silva 001 (CoRR, 2020)

Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (CoRR, 2020)

Taming callbacks for smart contract modularity. - Elvira Albert; Shelly Grossman; Noam Rinetzky; Clara Rodríguez-Núñez; Albert Rubio; Mooly Sagiv (Proc. ACM Program. Lang., 2020)

Lower-Bound Synthesis Using Loop Specialization and Max-SMT. - Elvira Albert; Samir Genaim; Enrique Martin-Martin; Alicia Merayo; Albert Rubio (CAV (2), 2021)

Actor-based model checking for Software-Defined Networks. - Elvira Albert; Miguel Gómez-Zamalloa; Miguel Isabel; Albert Rubio; Matteo Sammartino; Alexandra Silva 001 (J. Log. Algebraic Methods Program., 2021)

Don't run on fumes - Parametric gas bounds for smart contracts. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (J. Syst. Softw., 2021)

Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage". - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio (Zenodo, 2021)

Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage". - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio (Zenodo, 2021)

Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Clara Rodríguez-Núñez; Albert Rubio (IJCAR, 2022)

Distilling Constraints in Zero-Knowledge Protocols. - Elvira Albert; Marta Bellés-Muñoz; Miguel Isabel; Clara Rodríguez-Núñez; Albert Rubio (CAV (1), 2022)

A Max-SMT Superoptimizer for EVM handling Memory and Storage. - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio (TACAS (1), 2022)

Super-optimization of Smart Contracts. - Elvira Albert; Pablo Gordillo; Alejandro Hernández-Cerezo; Albert Rubio; Maria Anna Schett (ACM Trans. Softw. Eng. Methodol., 2022)

Inferring Needless Write Memory Accesses on Ethereum Bytecode. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (TACAS (1), 2023)

Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version). - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (CoRR, 2023)

Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. - Elvira Albert; Shelly Grossman; Noam Rinetzky; Clara Rodríguez-Núñez; Albert Rubio; Mooly Sagiv (IEEE Trans. Dependable Secur. Comput., 2023)

Circom: A Circuit Description Language for Building Zero-Knowledge Applications. - Marta Bellés-Muñoz; Miguel Isabel; Jose Luis Muñoz-Tapia; Albert Rubio; Jordi Baylina Melé (IEEE Trans. Dependable Secur. Comput., 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (Zenodo, 2023)

Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (ISSTA, 2024)

Scalable Verification of Zero-Knowledge Protocols. - Miguel Isabel; Clara Rodríguez-Núñez; Albert Rubio (SP, 2024)

SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. - Elvira Albert; Maria Garcia de la Banda; Alejandro Hernández-Cerezo; Alexey Ignatiev; Albert Rubio; Peter J. Stuckey (Proc. ACM Program. Lang., 2024)

Artifact for "SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-based, and SAT Techniques". - Elvira Albert; Maria Garcia de la Banda; Alejandro Hernández-Cerezo; Alexey Ignatiev; Albert Rubio; Peter J. Stuckey (Zenodo, 2024)

Neural-guided superoptimization in ethereum. - Matheus Araújo Aguiar; Elvira Albert; Samir Genaim; Pablo Gordillo; Alejandro Hernández-Cerezo; Daniel Kirchner; Albert Rubio (Inf. Softw. Technol., 2025)

Harnessing heap analysis for the synthesis of superoptimized bytecode. - Elvira Albert; Jesús Correas; Pablo Gordillo; Guillermo Román-Díez; Albert Rubio (J. Syst. Softw., 2025)