Albert Rubio

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