default search action
Albert Rubio
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j22]Elvira Albert
, Maria Garcia de la Banda
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. Proc. ACM Program. Lang. 8(PLDI): 1437-1462 (2024) - [c55]Elvira Albert
Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT. ISSTA 2024: 1186-1197 - [c54]Miguel Isabel, Clara Rodríguez-Núñez, Albert Rubio:
Scalable Verification of Zero-Knowledge Protocols. SP 2024: 1794-1812 - [d10]Elvira Albert
Artifact for "SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-based, and SAT Techniques". Zenodo, 2024 - 2023
- [j21]Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez
Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. IEEE Trans. Dependable Secur. Comput. 20(3): 2256-2273 (2023) - [j20]Marta Bellés-Muñoz
Circom: A Circuit Description Language for Building Zero-Knowledge Applications. IEEE Trans. Dependable Secur. Comput. 20(6): 4733-4751 (2023) - [c53]Elvira Albert
Inferring Needless Write Memory Accesses on Ethereum Bytecode. TACAS (1) 2023: 448-466 - [d9]Elvira Albert
Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". Zenodo, 2023 - [d8]Elvira Albert
Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". Zenodo, 2023 - [d7]Elvira Albert
Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". Zenodo, 2023 - [d6]Elvira Albert
Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". Zenodo, 2023 - [d5]Elvira Albert
Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". Zenodo, 2023 - [d4]Elvira Albert
Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". Zenodo, 2023 - [d3]Elvira Albert
Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode". Zenodo, 2023 - [i13]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 abs/2301.04757 (2023) - 2022
- [j19]Elvira Albert, Pablo Gordillo
Super-optimization of Smart Contracts. ACM Trans. Softw. Eng. Methodol. 31(4): 70:1-70:29 (2022) - [c52]Elvira Albert
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. IJCAR 2022: 3-7 - [c51]Elvira Albert
Distilling Constraints in Zero-Knowledge Protocols. CAV (1) 2022: 430-443 - [c50]Elvira Albert
A Max-SMT Superoptimizer for EVM handling Memory and Storage. TACAS (1) 2022: 201-219 - 2021
- [j18]Elvira Albert, Miguel Gómez-Zamalloa
Actor-based model checking for Software-Defined Networks. J. Log. Algebraic Methods Program. 118: 100617 (2021) - [j17]Elvira Albert
Don't run on fumes - Parametric gas bounds for smart contracts. J. Syst. Softw. 176: 110923 (2021) - [c49]Elvira Albert
Lower-Bound Synthesis Using Loop Specialization and Max-SMT. CAV (2) 2021: 863-886 - [d2]Elvira Albert
Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage". Zenodo, 2021 - [d1]Elvira Albert
Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage". Zenodo, 2021 - 2020
- [j16]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): 209:1-209:30 (2020) - [c48]Elvira Albert
Synthesis of Super-Optimized Smart Contracts Using Max-SMT. CAV (1) 2020: 177-200 - [c47]Elvira Albert, Jesús Correas
Smart, and also Reliable and Gas-Efficient, Contracts. ICST 2020: 2 - [c46]Elvira Albert
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. TACAS (2) 2020: 118-125 - [i12]Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, Albert Rubio, Matteo Sammartino, Alexandra Silva:
Actor-Based Model Checking for SDN Networks. CoRR abs/2001.10022 (2020) - [i11]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 abs/2004.14437 (2020) - [i10]Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. CoRR abs/2008.13601 (2020)
2010 – 2019
- 2019
- [j15]Cristina Borralleras
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. ACM Trans. Comput. Log. 20(4): 25:1-25:36 (2019) - [j14]Elvira Albert, Miquel Bofill
Resource Analysis driven by (Conditional) Termination Proofs. Theory Pract. Log. Program. 19(5-6): 722-739 (2019) - [c45]Elvira Albert, Jesús Correas
SAFEVM: a safety verifier for Ethereum smart contracts. ISSTA 2019: 386-389 - [c44]Jürgen Giesl
The Termination and Complexity Competition. TACAS (3) 2019: 156-166 - [c43]Elvira Albert, Pablo Gordillo
Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. VECoS 2019: 63-78 - [i9]Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio:
SAFEVM: A Safety Verifier for Ethereum Smart Contracts. CoRR abs/1906.04984 (2019) - [i8]Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin, Albert Rubio:
Resource Analysis driven by (Conditional) Termination Proofs. CoRR abs/1907.10096 (2019) - [i7]Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio:
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. CoRR abs/1912.11929 (2019) - 2018
- [c42]Elvira Albert, Pablo Gordillo
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. ATVA 2018: 513-520 - [c41]Elvira Albert
Constrained Dynamic Partial Order Reduction. CAV (2) 2018: 392-410 - [c40]Elvira Albert, Miguel Gómez-Zamalloa
SDN-Actors: Modeling and Verification of SDN Programs. FM 2018: 550-567 - [i6]Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey:
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. CoRR abs/1805.07208 (2018) - [i5]Elvira Albert, Pablo Gordillo
GASTAP: A Gas Analyzer for Smart Contracts. CoRR abs/1811.10403 (2018) - 2017
- [c39]Cristina Borralleras
Proving Termination Through Conditional Termination. TACAS (1) 2017: 99-117 - 2016
- [c38]Lorenzo Candeago
Speeding up the Constraint-Based Method in Difference Logic. SAT 2016: 284-301 - 2015
- [j13]Frédéric Blanqui
The computability path ordering. Log. Methods Comput. Sci. 11(4) (2015) - [j12]Jean-Pierre Jouannaud, Albert Rubio:
Normal Higher-Order Termination. ACM Trans. Comput. Log. 16(2): 13:1-13:38 (2015) - [c37]Jürgen Giesl
Termination Competition (termCOMP 2015). CADE 2015: 105-108 - [c36]Marc Brockschmidt, Daniel Larraz
Compositional Safety Verification with Max-SMT. FMCAD 2015: 33-40 - [i4]Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Compositional Safety Verification with Max-SMT. CoRR abs/1507.03851 (2015) - 2014
- [c35]Daniel Larraz
Proving Non-termination Using Max-SMT. CAV 2014: 779-796 - [c34]Daniel Larraz
Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. SAT 2014: 333-350 - 2013
- [j11]Miquel Bofill
Paramodulation with Non-Monotonic Orderings and Simplification. J. Autom. Reason. 50(1): 51-98 (2013) - [j10]Miquel Bofill
The recursive path and polynomial ordering for first-order and higher-order terms. J. Log. Comput. 23(1): 263-305 (2013) - [c33]Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Proving termination of imperative programs using Max-SMT. FMCAD 2013: 218-225 - [c32]Daniel Larraz
SMT-Based Array Invariant Generation. VMCAI 2013: 169-188 - 2012
- [j9]Cristina Borralleras
SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. J. Autom. Reason. 48(1): 107-131 (2012) - [c31]Maribel Fernández
Nominal Completion for Rewrite Systems with Binders. ICALP (2) 2012: 201-213
2000 – 2009
- 2009
- [j8]Miquel Bofill
Paramodulation with Well-founded Orderings. J. Log. Comput. 19(2): 263-302 (2009) - [c30]Cristina Borralleras
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. CADE 2009: 294-305 - 2008
- [c29]Miquel Bofill
The Barcelogic SMT Solver. CAV 2008: 294-298 - [c28]Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio:
The Computability Path Ordering: The End of a Quest. CSL 2008: 1-14 - [c27]Miquel Bofill
A Write-Based Solver for SAT Modulo the Theory of Arrays. FMCAD 2008: 1-8 - [i3]Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio:
The computability path ordering: the end of a quest. CoRR abs/0806.2517 (2008) - 2007
- [j7]Jean-Pierre Jouannaud, Albert Rubio:
Polymorphic higher-order recursive path orderings. J. ACM 54(1): 2:1-2:48 (2007) - [c26]Cristina Borralleras
Orderings and Constraints: Theory and Practice of Proving Termination. Rewriting, Computation and Proof 2007: 28-43 - [c25]Frédéric Blanqui
HORPO with Computability Closure: A Reconstruction. LPAR 2007: 138-150 - [c24]Robert Nieuwenhuis, Albert Oliveras
Challenges in Satisfiability Modulo Theories. RTA 2007: 2-18 - [i2]Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio:
HORPO with Computability Closure : A Reconstruction. CoRR abs/0708.3582 (2007) - 2006
- [c23]Frédéric Blanqui
Higher-Order Termination: From Kruskal to Computability. LPAR 2006: 1-14 - [c22]Jean-Pierre Jouannaud, Albert Rubio:
Higher-Order Orderings for Normal Rewriting. RTA 2006: 387-399 - [i1]Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio:
Higher-Order Termination: from Kruskal to Computability. CoRR abs/cs/0609039 (2006) - 2005
- [c21]Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio:
Recursive Path Orderings Can Also Be Incremental. LPAR 2005: 230-245 - [c20]Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio:
Orderings for Innermost Termination. RTA 2005: 17-31 - 2004
- [c19]Miquel Bofill, Albert Rubio:
Redundancy Notions for Paramodulation with Non-monotonic Orderings. IJCAR 2004: 107-121 - 2003
- [j6]Miquel Bofill
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. J. Autom. Reason. 30(1): 99-120 (2003) - [c18]Cristina Borralleras
Monotonic AC-Compatible Semantic Path Orderings. RTA 2003: 279-295 - 2002
- [j5]Albert Rubio:
A Fully Syntactic AC-RPO. Inf. Comput. 178(2): 515-533 (2002) - [c17]Cristina Borralleras
Recursive Path Orderings Can Be Context-Sensitive. CADE 2002: 314-331 - [c16]Miquel Bofill
Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. CADE 2002: 456-470 - 2001
- [c15]Cristina Borralleras
A Monotonic Higher-Order Semantic Path Ordering. LPAR 2001: 531-547 - [p1]Robert Nieuwenhuis
Paramodulation-Based Theorem Proving. Handbook of Automated Reasoning 2001: 371-443 - 2000
- [c14]Cristina Borralleras
Complete Monotonic Semantic Path Orderings. CADE 2000: 346-364 - [c13]Miquel Bofill
Modular Redundancy for Theorem Proving. FroCoS 2000: 186-199
1990 – 1999
- 1999
- [c12]Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis
Paramodulation with Non-Monotonic Orderings. LICS 1999: 225-233 - [c11]Jean-Pierre Jouannaud, Albert Rubio:
The Higher-Order Recursive Path Ordering. LICS 1999: 402-411 - [c10]Albert Rubio:
A Fully Syntactic AC-RPO. RTA 1999: 133-147 - 1998
- [j4]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): 33-58 (1998) - 1997
- [j3]Robert Nieuwenhuis
Paramodulation with Built-in AC-Theories and Symbolic Constraints. J. Symb. Comput. 23(1): 1-21 (1997) - 1996
- [c9]Jean-Pierre Jouannaud, Albert Rubio:
A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form. RTA 1996: 108-122 - 1995
- [j2]Robert Nieuwenhuis
Theorem Proving with Ordering and Equality Constrained Clauses. J. Symb. Comput. 19(4): 321-351 (1995) - [j1]Albert Rubio, Robert Nieuwenhuis
A Total AC-Compatible Ordering Based on RPO. Theor. Comput. Sci. 142(2): 209-227 (1995) - [c8]Albert Rubio:
Theorem Proving modulo Associativity. CSL 1995: 452-467 - [c7]Albert Rubio:
Extension Orderings. ICALP 1995: 511-522 - [c6]Hubert Comon, Robert Nieuwenhuis
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract). LICS 1995: 375-385 - [e1]Robert Nieuwenhuis, Albert Rubio:
9th International Workshop on Unification, UNIF 1995, Sitges, Spain, April 2-3, 1995. 1995 [contents] - 1994
- [c5]Robert Nieuwenhuis, Albert Rubio:
AC-Superposition with Constraints: No AC-Unifiers Needed. CADE 1994: 545-559 - 1993
- [c4]Albert Rubio, Robert Nieuwenhuis:
A Precedence-Based Total AC-Compatible Ordering. RTA 1993: 374-388 - 1992
- [c3]Robert Nieuwenhuis, Albert Rubio:
Theorem Proving with Ordering Constrained Clauses. CADE 1992: 477-491 - [c2]Robert Nieuwenhuis, Albert Rubio:
Basic Superposition is Complete. ESOP 1992: 371-389 - 1990
- [c1]Robert Nieuwenhuis, Fernando Orejas, Albert Rubio:
TRIP: An Implementation of Clausal Rewriting. CADE 1990: 667-668
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-25 22:44 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: