Albert Rubio

Maria Garcia de la Banda

Alexey Ignatiev

Peter J. Stuckey

Dataset, March, 2024

SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques.

[BibT_eX]

[DOI]

Maria Garcia de la Banda

Alexey Ignatiev

Peter J. Stuckey

Proc. ACM Program. Lang., 2024

Scalable Verification of Zero-Knowledge Protocols.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2024

2023

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode".

[BibT_eX]

[DOI]

Dataset, October, 2023

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode".

[BibT_eX]

[DOI]

Dataset, October, 2023

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode".

[BibT_eX]

[DOI]

Dataset, October, 2023

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode".

[BibT_eX]

[DOI]

Dataset, October, 2023

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode".

[BibT_eX]

[DOI]

Dataset, October, 2023

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode".

[BibT_eX]

[DOI]

Dataset, October, 2023

Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode".

[BibT_eX]

[DOI]

Dataset, October, 2023

Circom: A Circuit Description Language for Building Zero-Knowledge Applications.

[BibT_eX]

[DOI]

Marta Bellés-Muñoz

Jose Luis Muñoz-Tapia

Jordi Baylina Melé

IEEE Trans. Dependable Secur. Comput., 2023

Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks.

[BibT_eX]

[DOI]

Shelly Grossman

Noam Rinetzky

Mooly Sagiv

IEEE Trans. Dependable Secur. Comput., 2023

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

[BibT_eX]

[DOI]

CoRR, 2023

Inferring Needless Write Memory Accesses on Ethereum Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

2022

Super-optimization of Smart Contracts.

[BibT_eX]

[DOI]

Maria Anna Schett

ACM Trans. Softw. Eng. Methodol., 2022

A Max-SMT Superoptimizer for EVM handling Memory and Storage.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Distilling Constraints in Zero-Knowledge Protocols.

[BibT_eX]

[DOI]

Marta Bellés-Muñoz

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage".

[BibT_eX]

[DOI]

Dataset, November, 2021

Artifact for paper "A Max-SMT Superoptimizer for EVM handling Memory and Storage".

[BibT_eX]

[DOI]

Dataset, November, 2021

Don't run on fumes - Parametric gas bounds for smart contracts.

[BibT_eX]

[DOI]

J. Syst. Softw., 2021

Actor-based model checking for Software-Defined Networks.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2021

Lower-Bound Synthesis Using Loop Specialization and Max-SMT.

[BibT_eX]

[DOI]

Samir Genaim

Enrique Martin-Martin

Alicia Merayo

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Taming callbacks for smart contract modularity.

[BibT_eX]

[DOI]

Shelly Grossman

Noam Rinetzky

Mooly Sagiv

Proc. ACM Program. Lang., 2020

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

[BibT_eX]

[DOI]

CoRR, 2020

Actor-Based Model Checking for SDN Networks.

[BibT_eX]

[DOI]

CoRR, 2020

GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Smart, and also Reliable and Gas-Efficient, Contracts.

[BibT_eX]

[DOI]

Proceedings of the 13th IEEE International Conference on Software Testing, 2020

Synthesis of Super-Optimized Smart Contracts Using Max-SMT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Resource Analysis driven by (Conditional) Termination Proofs.

[BibT_eX]

[DOI]

Enrique Martin-Martin

Theory Pract. Log. Program., 2019

Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2019

Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis.

[BibT_eX]

[DOI]

Proceedings of the Verification and Evaluation of Computer and Communication Systems, 2019

The Termination and Complexity Competition.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

SAFEVM: a safety verifier for Ethereum smart contracts.

[BibT_eX]

[DOI]

Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2019

2018

GASTAP: A Gas Analyzer for Smart Contracts.

[BibT_eX]

[DOI]

CoRR, 2018

SDN-Actors: Modeling and Verification of SDN Programs.

[BibT_eX]

[DOI]

Matteo Sammartino

Alexandra Silva

Proceedings of the Formal Methods - 22nd International Symposium, 2018

Constrained Dynamic Partial Order Reduction.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

EthIR: A Framework for High-Level Analysis of Ethereum Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2018

2017

Proving Termination Through Conditional Termination.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

2016

Speeding up the Constraint-Based Method in Difference Logic.

[BibT_eX]

[DOI]

Lorenzo Candeago

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

2015

Normal Higher-Order Termination.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2015

The computability path ordering.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2015

Compositional Safety Verification with Max-SMT.

[BibT_eX]

[DOI]

Marc Brockschmidt

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Termination Competition (termCOMP 2015).

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Proving Non-termination Using Max-SMT.

[BibT_eX]

[DOI]

Kaustubh Nimkar

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

The recursive path and polynomial ordering for first-order and higher-order terms.

[BibT_eX]

[DOI]

J. Log. Comput., 2013

Paramodulation with Non-Monotonic Orderings and Simplification.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

SMT-Based Array Invariant Generation.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

Proving termination of imperative programs using Max-SMT.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints.

[BibT_eX]

[DOI]

Salvador Lucas

J. Autom. Reason., 2012

Nominal Completion for Rewrite Systems with Binders.

[BibT_eX]

[DOI]

Maribel Fernández

Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

2009

Paramodulation with Well-founded Orderings.

[BibT_eX]

[DOI]

J. Log. Comput., 2009

Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic.

[BibT_eX]

[DOI]

Salvador Lucas

Rafael Navarro-Marset

Proceedings of the Automated Deduction, 2009

2008

A Write-Based Solver for SAT Modulo the Theory of Arrays.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2008

The Computability Path Ordering: The End of a Quest.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

The Barcelogic SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Polymorphic higher-order recursive path orderings.

[BibT_eX]

[DOI]

J. ACM, 2007

Challenges in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

HORPO with Computability Closure: A Reconstruction.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2007

Orderings and Constraints: Theory and Practice of Proving Termination.

[BibT_eX]

[DOI]

Proceedings of the Rewriting, 2007

2006

Higher-Order Orderings for Normal Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Higher-Order Termination: From Kruskal to Computability.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

2005

Orderings for Innermost Termination.

[BibT_eX]

[DOI]

Mirtha-Lina Fernández

Guillem Godoy

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Recursive Path Orderings Can Also Be Incremental.

[BibT_eX]

[DOI]

Mirtha-Lina Fernández

Guillem Godoy

Proceedings of the Logic for Programming, 2005

2004

Redundancy Notions for Paramodulation with Non-monotonic Orderings.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

Monotonic AC-Compatible Semantic Path Orderings.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002

A Fully Syntactic AC-RPO.

[BibT_eX]

[DOI]

Inf. Comput., 2002

Recursive Path Orderings Can Be Context-Sensitive.

[BibT_eX]

[DOI]

Salvador Lucas

Proceedings of the Automated Deduction, 2002

Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

2001

A Monotonic Higher-Order Semantic Path Ordering.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2001

Paramodulation-Based Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Modular Redundancy for Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2000

Complete Monotonic Semantic Path Orderings.

[BibT_eX]

[DOI]

Maria Ferreira

Proceedings of the Automated Deduction, 2000

1999

The Higher-Order Recursive Path Ordering.

[BibT_eX]

[DOI]

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Paramodulation with Non-Monotonic Orderings.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1998

1997

Paramodulation with Built-in AC-Theories and Symbolic Constraints.

[BibT_eX]

[DOI]

J. Symb. Comput., 1997

1996

A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

1995

A Total AC-Compatible Ordering Based on RPO.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

Theorem Proving with Ordering and Equality Constrained Clauses.

[BibT_eX]

[DOI]

J. Symb. Comput., 1995

Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract)

[BibT_eX]

[DOI]

Hubert Comon

Proceedings of the Proceedings, 1995

Extension Orderings.

[BibT_eX]

[DOI]

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

Theorem Proving modulo Associativity.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

AC-Superposition with Constraints: No AC-Unifiers Needed.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

1992

Basic Superposition is Complete.

[BibT_eX]

[DOI]

Proceedings of the ESOP '92, 1992

Theorem Proving with Ordering Constrained Clauses.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1990

TRIP: An Implementation of Clausal Rewriting.

[BibT_eX]

[DOI]

Fernando Orejas