Albert Rubio
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
47
Venues
18
Active years
1990–2025
Best venue rank
A*
Where they publish
Papers
47 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | SEFM | Securely Optimized (Ethereum) Smart Contracts Using Formal Methods. | Elvira Albert, Samir Genaim, Pablo Gordillo, Alejandro Hernndez-Cerezo, Enrique Martin-Martin, Albert Rubio |
| 2024 | ISSTA | Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2024 | SP | Scalable Verification of Zero-Knowledge Protocols. | Miguel Isabel, Clara Rodrguez-Nez, Albert Rubio |
| 2023 | TACAS | Inferring Needless Write Memory Accesses on Ethereum Bytecode. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2022 | CADE | Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. | Elvira Albert, Pablo Gordillo, Alejandro Hernndez-Cerezo, Clara Rodrguez-Nez, Albert Rubio |
| 2022 | CAV | Distilling Constraints in Zero-Knowledge Protocols. | Elvira Albert, Marta Bells-Muoz, Miguel Isabel, Clara Rodrguez-Nez, Albert Rubio |
| 2022 | TACAS | A Max-SMT Superoptimizer for EVM handling Memory and Storage. | Elvira Albert, Pablo Gordillo, Alejandro Hernndez-Cerezo, Albert Rubio |
| 2021 | CAV | Lower-Bound Synthesis Using Loop Specialization and Max-SMT. | Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo, Albert Rubio |
| 2020 | CAV | Synthesis of Super-Optimized Smart Contracts Using Max-SMT. | Elvira Albert, Pablo Gordillo, Albert Rubio, Maria Anna Schett |
| 2020 | ICST | Smart, and also Reliable and Gas-Efficient, Contracts. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2020 | TACAS | GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2019 | ISSTA | SAFEVM: a safety verifier for Ethereum smart contracts. | Elvira Albert, Jess Correas, Pablo Gordillo, Guillermo Romn-Dez, Albert Rubio |
| 2019 | TACAS | The Termination and Complexity Competition. | Jrgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada |
| 2019 | VECoS | Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. | Elvira Albert, Pablo Gordillo, Albert Rubio, Ilya Sergey |
| 2018 | ATVA | EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. | Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey |
| 2018 | CAV | Constrained Dynamic Partial Order Reduction. | Elvira Albert, Miguel Gmez-Zamalloa, Miguel Isabel, Albert Rubio |
| 2018 | FM | SDN-Actors: Modeling and Verification of SDN Programs. | Elvira Albert, Miguel Gmez-Zamalloa, Albert Rubio, Matteo Sammartino, Alexandra Silva |
| 2017 | TACAS | Proving Termination Through Conditional Termination. | Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2016 | SAT | Speeding up the Constraint-Based Method in Difference Logic. | Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2015 | CADE | Termination Competition (termCOMP 2015). | Jrgen Giesl, Frdric Mesnard, Albert Rubio, Ren Thiemann, Johannes Waldmann |
| 2015 | FMCAD | Compositional Safety Verification with Max-SMT. | Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2014 | CAV | Proving Non-termination Using Max-SMT. | Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2014 | SAT | Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. | Daniel Larraz, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2013 | FMCAD | Proving termination of imperative programs using Max-SMT. | Daniel Larraz, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2013 | VMCAI | SMT-Based Array Invariant Generation. | Daniel Larraz, Enric Rodrguez-Carbonell, Albert Rubio |
| 2012 | ICALP | Nominal Completion for Rewrite Systems with Binders. | Maribel Fernndez, Albert Rubio |
| 2009 | CADE | Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. | Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodrguez-Carbonell, Albert Rubio |
| 2008 | CAV | The Barcelogic SMT Solver. | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2008 | CSL | The Computability Path Ordering: The End of a Quest. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2008 | FMCAD | A Write-Based Solver for SAT Modulo the Theory of Arrays. | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2007 | LPAR | HORPO with Computability Closure: A Reconstruction. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2006 | LPAR | Higher-Order Termination: From Kruskal to Computability. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2005 | LPAR | Recursive Path Orderings Can Also Be Incremental. | Mirtha-Lina Fernndez, Guillem Godoy, Albert Rubio |
| 2004 | CADE | Redundancy Notions for Paramodulation with Non-monotonic Orderings. | Miquel Bofill, Albert Rubio |
| 2002 | CADE | Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. | Miquel Bofill, Albert Rubio |
| 2002 | CADE | Recursive Path Orderings Can Be Context-Sensitive. | Cristina Borralleras, Salvador Lucas, Albert Rubio |
| 2001 | LPAR | A Monotonic Higher-Order Semantic Path Ordering. | Cristina Borralleras, Albert Rubio |
| 2000 | CADE | Complete Monotonic Semantic Path Orderings. | Cristina Borralleras, Maria Ferreira, Albert Rubio |
| 1999 | LICS | Paramodulation with Non-Monotonic Orderings. | Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio |
| 1999 | LICS | The Higher-Order Recursive Path Ordering. | Jean-Pierre Jouannaud, Albert Rubio |
| 1995 | CSL | Theorem Proving modulo Associativity. | Albert Rubio |
| 1995 | ICALP | Extension Orderings. | Albert Rubio |
| 1995 | LICS | Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) | Hubert Comon, Robert Nieuwenhuis, Albert Rubio |
| 1994 | CADE | AC-Superposition with Constraints: No AC-Unifiers Needed. | Robert Nieuwenhuis, Albert Rubio |
| 1992 | CADE | Theorem Proving with Ordering Constrained Clauses. | Robert Nieuwenhuis, Albert Rubio |
| 1992 | ESOP | Basic Superposition is Complete. | Robert Nieuwenhuis, Albert Rubio |
| 1990 | CADE | TRIP: An Implementation of Clausal Rewriting. | Robert Nieuwenhuis, Fernando Orejas, Albert Rubio |