Albert Rubio

Orcid: 0000-0002-0501-9830

According to our database1, Albert Rubio authored at least 84 papers between 1990 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Artifact for "SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-based, and SAT Techniques".
Dataset, March, 2024

SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques.
Proc. ACM Program. Lang., 2024

Scalable Verification of Zero-Knowledge Protocols.
Proceedings of the IEEE Symposium on Security and Privacy, 2024

Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT.
Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2024

2023
Circom: A Circuit Description Language for Building Zero-Knowledge Applications.
IEEE Trans. Dependable Secur. Comput., 2023

Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks.
IEEE Trans. Dependable Secur. Comput., 2023

Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version).
CoRR, 2023

Inferring Needless Write Memory Accesses on Ethereum Bytecode.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

2022
Super-optimization of Smart Contracts.
ACM Trans. Softw. Eng. Methodol., 2022

A Max-SMT Superoptimizer for EVM handling Memory and Storage.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Distilling Constraints in Zero-Knowledge Protocols.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage".
Dataset, November, 2021

Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage".
Dataset, November, 2021

<i>Don't run on fumes</i> - Parametric gas bounds for smart contracts.
J. Syst. Softw., 2021

Actor-based model checking for Software-Defined Networks.
J. Log. Algebraic Methods Program., 2021

Lower-Bound Synthesis Using Loop Specialization and Max-SMT.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020
Taming callbacks for smart contract modularity.
Proc. ACM Program. Lang., 2020

Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph.
CoRR, 2020

Actor-Based Model Checking for SDN Networks.
CoRR, 2020

GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Smart, and also Reliable and Gas-Efficient, Contracts.
Proceedings of the 13th IEEE International Conference on Software Testing, 2020

Synthesis of Super-Optimized Smart Contracts Using Max-SMT.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Resource Analysis driven by (Conditional) Termination Proofs.
Theory Pract. Log. Program., 2019

Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers.
ACM Trans. Comput. Log., 2019

Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis.
Proceedings of the Verification and Evaluation of Computer and Communication Systems, 2019

The Termination and Complexity Competition.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

SAFEVM: a safety verifier for Ethereum smart contracts.
Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2019

2018
GASTAP: A Gas Analyzer for Smart Contracts.
CoRR, 2018

SDN-Actors: Modeling and Verification of SDN Programs.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

Constrained Dynamic Partial Order Reduction.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode.
Proceedings of the Automated Technology for Verification and Analysis, 2018

2017
Proving Termination Through Conditional Termination.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

2016
Speeding up the Constraint-Based Method in Difference Logic.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

2015
Normal Higher-Order Termination.
ACM Trans. Comput. Log., 2015

The computability path ordering.
Log. Methods Comput. Sci., 2015

Compositional Safety Verification with Max-SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Termination Competition (termCOMP 2015).
Proceedings of the Automated Deduction - CADE-25, 2015

2014
Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Proving Non-termination Using Max-SMT.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
The recursive path and polynomial ordering for first-order and higher-order terms.
J. Log. Comput., 2013

Paramodulation with Non-Monotonic Orderings and Simplification.
J. Autom. Reason., 2013

SMT-Based Array Invariant Generation.
Proceedings of the Verification, 2013

Proving termination of imperative programs using Max-SMT.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012
SAT Modulo Linear Arithmetic for Solving Polynomial Constraints.
J. Autom. Reason., 2012

Nominal Completion for Rewrite Systems with Binders.
Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

2009
Paramodulation with Well-founded Orderings.
J. Log. Comput., 2009

Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic.
Proceedings of the Automated Deduction, 2009

2008
A Write-Based Solver for SAT Modulo the Theory of Arrays.
Proceedings of the Formal Methods in Computer-Aided Design, 2008

The Computability Path Ordering: The End of a Quest.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

The Barcelogic SMT Solver.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Polymorphic higher-order recursive path orderings.
J. ACM, 2007

Challenges in Satisfiability Modulo Theories.
Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

HORPO with Computability Closure: A Reconstruction.
Proceedings of the Logic for Programming, 2007

Orderings and Constraints: Theory and Practice of Proving Termination.
Proceedings of the Rewriting, 2007

2006
Higher-Order Orderings for Normal Rewriting.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Higher-Order Termination: From Kruskal to Computability.
Proceedings of the Logic for Programming, 2006

2005
Orderings for Innermost Termination.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Recursive Path Orderings Can Also Be Incremental.
Proceedings of the Logic for Programming, 2005

2004
Redundancy Notions for Paramodulation with Non-monotonic Orderings.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings.
J. Autom. Reason., 2003

Monotonic AC-Compatible Semantic Path Orderings.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002
A Fully Syntactic AC-RPO.
Inf. Comput., 2002

Recursive Path Orderings Can Be Context-Sensitive.
Proceedings of the Automated Deduction, 2002

Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation.
Proceedings of the Automated Deduction, 2002

2001
A Monotonic Higher-Order Semantic Path Ordering.
Proceedings of the Logic for Programming, 2001

Paramodulation-Based Theorem Proving.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000
Modular Redundancy for Theorem Proving.
Proceedings of the Frontiers of Combining Systems, 2000

Complete Monotonic Semantic Path Orderings.
Proceedings of the Automated Deduction, 2000

1999
The Higher-Order Recursive Path Ordering.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Paramodulation with Non-Monotonic Orderings.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998
Rewrite Orderings for Higher-Order Terms in eta-Long beta-Normal Form and Recursive Path Ordering.
Theor. Comput. Sci., 1998

1997
Paramodulation with Built-in AC-Theories and Symbolic Constraints.
J. Symb. Comput., 1997

1996
A Recursive Path Ordering for Higher-Order Terms in <i>eta</i>-Long <i>beta</i>-Normal Form.
Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

1995
A Total AC-Compatible Ordering Based on RPO.
Theor. Comput. Sci., 1995

Theorem Proving with Ordering and Equality Constrained Clauses.
J. Symb. Comput., 1995

Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract)
Proceedings of the Proceedings, 1995

Extension Orderings.
Proceedings of the Automata, Languages and Programming, 22nd International Colloquium, 1995

Theorem Proving modulo Associativity.
Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994
AC-Superposition with Constraints: No AC-Unifiers Needed.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993
A Precedence-Based Total AC-Compatible Ordering.
Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

1992
Basic Superposition is Complete.
Proceedings of the ESOP '92, 1992

Theorem Proving with Ordering Constrained Clauses.
Proceedings of the Automated Deduction, 1992

1990
TRIP: An Implementation of Clausal Rewriting.
Proceedings of the 10th International Conference on Automated Deduction, 1990


  Loading...