Albert Rubio

Publication Activity (10 Years)

Years Active: 1990-2024
Publications (10 Years): 34

Top Topics

Partial Order Reduction

Description Language

Rewrite Systems

Top Venues

Proc. ACM Program. Lang.

Publications

Elvira Albert, Maria Garcia de la Banda, Alejandro Hernández-Cerezo, Alexey Ignatiev, Albert Rubio, Peter J. Stuckey
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. IEEE Trans. Dependable Secur. Comput. 20 (3) (2023)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Inferring Needless Write Memory Accesses on Ethereum Bytecode. TACAS (1) (2023)
Marta Bellés-Muñoz, Miguel Isabel, Jose Luis Muñoz-Tapia, Albert Rubio, Jordi Baylina Melé
Circom: A Circuit Description Language for Building Zero-Knowledge Applications. IEEE Trans. Dependable Secur. Comput. 20 (6) (2023)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version). CoRR (2023)
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez, Albert Rubio
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. IJCAR (2022)
Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez, Albert Rubio
Distilling Constraints in Zero-Knowledge Protocols. CAV (1) (2022)
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio, Maria Anna Schett
Super-optimization of Smart Contracts. ACM Trans. Softw. Eng. Methodol. 31 (4) (2022)
Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio
A Max-SMT Superoptimizer for EVM handling Memory and Storage. TACAS (1) (2022)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
- Parametric gas bounds for smart contracts. J. Syst. Softw. 176 (2021)
Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo, Albert Rubio
Lower-Bound Synthesis Using Loop Specialization and Max-SMT. CAV (2) (2021)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, Alexandra Silva
Actor-based model checking for Software-Defined Networks. J. Log. Algebraic Methods Program. 118 (2021)
Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. CoRR (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Smart, and also Reliable and Gas-Efficient, Contracts. ICST (2020)
Elvira Albert, Pablo Gordillo, Albert Rubio, Maria Anna Schett
Synthesis of Super-Optimized Smart Contracts Using Max-SMT. CAV (1) (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph. CoRR (2020)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, Alexandra Silva
Actor-Based Model Checking for SDN Networks. CoRR (2020)
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
Taming callbacks for smart contract modularity. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. TACAS (2) (2020)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
SAFEVM: a safety verifier for Ethereum smart contracts. ISSTA (2019)
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. VECoS (2019)
Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio
Resource Analysis driven by (Conditional) Termination Proofs. Theory Pract. Log. Program. 19 (5-6) (2019)
Cristina Borralleras, Daniel Larraz, Enric Rodríguez-Carbonell, Albert Oliveras, Albert Rubio
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. ACM Trans. Comput. Log. 20 (4) (2019)
Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
The Termination and Complexity Competition. TACAS (3) (2019)
Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio
Resource Analysis driven by (Conditional) Termination Proofs. CoRR (2019)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. CoRR (2019)
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
SAFEVM: A Safety Verifier for Ethereum Smart Contracts. CoRR (2019)
Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey
GASTAP: A Gas Analyzer for Smart Contracts. CoRR (2018)
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. ATVA (2018)
Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio
Constrained Dynamic Partial Order Reduction. CAV (2) (2018)
Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. CoRR (2018)
Elvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, Matteo Sammartino, Alexandra Silva
SDN-Actors: Modeling and Verification of SDN Programs. FM (2018)
Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Proving Termination Through Conditional Termination. TACAS (1) (2017)
Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Speeding up the Constraint-Based Method in Difference Logic. SAT (2016)
Jean-Pierre Jouannaud, Albert Rubio
Normal Higher-Order Termination. ACM Trans. Comput. Log. 16 (2) (2015)
Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Compositional Safety Verification with Max-SMT. FMCAD (2015)
Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Compositional Safety Verification with Max-SMT. CoRR (2015)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
The computability path ordering. Log. Methods Comput. Sci. 11 (4) (2015)
Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann
Termination Competition (termCOMP 2015). CADE (2015)
Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Proving Non-termination Using Max-SMT. CAV (2014)
Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. SAT (2014)
Daniel Larraz, Enric Rodríguez-Carbonell, Albert Rubio
SMT-Based Array Invariant Generation. VMCAI (2013)
Miquel Bofill, Albert Rubio
Paramodulation with Non-Monotonic Orderings and Simplification. J. Autom. Reason. 50 (1) (2013)
Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Proving termination of imperative programs using Max-SMT. FMCAD (2013)
Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, Albert Rubio
The recursive path and polynomial ordering for first-order and higher-order terms. J. Log. Comput. 23 (1) (2013)
Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. J. Autom. Reason. 48 (1) (2012)
Maribel Fernández, Albert Rubio
Nominal Completion for Rewrite Systems with Binders. ICALP (2) (2012)
Miquel Bofill, Albert Rubio
Paramodulation with Well-founded Orderings. J. Log. Comput. 19 (2) (2009)
Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell, Albert Rubio
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. CADE (2009)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
The computability path ordering: the end of a quest CoRR (2008)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
The Computability Path Ordering: The End of a Quest. CSL (2008)
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
The Barcelogic SMT Solver. CAV (2008)
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
A Write-Based Solver for SAT Modulo the Theory of Arrays. FMCAD (2008)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
HORPO with Computability Closure: A Reconstruction. LPAR (2007)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
HORPO with Computability Closure : A Reconstruction CoRR (2007)
Cristina Borralleras, Albert Rubio
Orderings and Constraints: Theory and Practice of Proving Termination. Rewriting, Computation and Proof (2007)
Jean-Pierre Jouannaud, Albert Rubio
Polymorphic higher-order recursive path orderings. J. ACM 54 (1) (2007)
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Challenges in Satisfiability Modulo Theories. RTA (2007)
Jean-Pierre Jouannaud, Albert Rubio
Higher-Order Orderings for Normal Rewriting. RTA (2006)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Higher-Order Termination: From Kruskal to Computability. LPAR (2006)
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Higher-Order Termination: from Kruskal to Computability CoRR (2006)
Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio
Orderings for Innermost Termination. RTA (2005)
Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio
Recursive Path Orderings Can Also Be Incremental. LPAR (2005)
Miquel Bofill, Albert Rubio
Redundancy Notions for Paramodulation with Non-monotonic Orderings. IJCAR (2004)
Cristina Borralleras, Albert Rubio
Monotonic AC-Compatible Semantic Path Orderings. RTA (2003)
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. J. Autom. Reason. 30 (1) (2003)
Albert Rubio
A Fully Syntactic AC-RPO. Inf. Comput. 178 (2) (2002)
Cristina Borralleras, Salvador Lucas, Albert Rubio
Recursive Path Orderings Can Be Context-Sensitive. CADE (2002)
Miquel Bofill, Albert Rubio
Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. CADE (2002)
Cristina Borralleras, Albert Rubio
A Monotonic Higher-Order Semantic Path Ordering. LPAR (2001)
Cristina Borralleras, Maria Ferreira, Albert Rubio
Complete Monotonic Semantic Path Orderings. CADE (2000)
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Modular Redundancy for Theorem Proving. FroCoS (2000)
Jean-Pierre Jouannaud, Albert Rubio
The Higher-Order Recursive Path Ordering. LICS (1999)
Albert Rubio
A Fully Syntactic AC-RPO. RTA (1999)
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Paramodulation with Non-Monotonic Orderings. LICS (1999)
Jean-Pierre Jouannaud, Albert Rubio
Rewrite Orderings for Higher-Order Terms in eta-Long beta-Normal Form and Recursive Path Ordering. Theor. Comput. Sci. 208 (1-2) (1998)
Robert Nieuwenhuis, Albert Rubio
Paramodulation with Built-in AC-Theories and Symbolic Constraints. J. Symb. Comput. 23 (1) (1997)
Jean-Pierre Jouannaud, Albert Rubio
-Normal Form. RTA (1996)
Albert Rubio, Robert Nieuwenhuis
A Total AC-Compatible Ordering Based on RPO. Theor. Comput. Sci. 142 (2) (1995)
Robert Nieuwenhuis, Albert Rubio
Theorem Proving with Ordering and Equality Constrained Clauses. J. Symb. Comput. 19 (4) (1995)
Hubert Comon, Robert Nieuwenhuis, Albert Rubio
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) LICS (1995)
Albert Rubio
Extension Orderings. ICALP (1995)
Albert Rubio
Theorem Proving modulo Associativity. CSL (1995)
Robert Nieuwenhuis, Albert Rubio
AC-Superposition with Constraints: No AC-Unifiers Needed. CADE (1994)
Albert Rubio, Robert Nieuwenhuis
A Precedence-Based Total AC-Compatible Ordering. RTA (1993)
Robert Nieuwenhuis, Albert Rubio
Basic Superposition is Complete. ESOP (1992)
Robert Nieuwenhuis, Albert Rubio
Theorem Proving with Ordering Constrained Clauses. CADE (1992)
Robert Nieuwenhuis, Fernando Orejas, Albert Rubio
TRIP: An Implementation of Clausal Rewriting. CADE (1990)