5 Search Results for "Hobor, Aquinas"

Document
DOI: 10.4230/LIPIcs.AFT.2025.23
Transaction Fee Market Design for Parallel Execution

Authors: Bahar Acilan, Andrei Constantinescu, Lioba Heimbach, and Roger Wattenhofer

Published in: LIPIcs, Volume 354, 7th Conference on Advances in Financial Technologies (AFT 2025)

Abstract
Given the low throughput of blockchains like Bitcoin and Ethereum, scalability - the ability to process an increasing number of transactions - has become a central focus of blockchain research. One promising approach is the parallelization of transaction execution across multiple threads. However, achieving efficient parallelization requires a redesign of the incentive structure within the fee market. Currently, the fee market does not differentiate between transactions that access multiple high-demand storage keys (i.e., unique identifiers for individual data entries) versus a single low-demand one, as long as they require the same computational effort. Addressing this discrepancy is crucial for enabling more effective parallel execution. In this work, we aim to bridge the gap between the current fee market and the need for parallel execution by exploring alternative fee market designs. To this end, we propose a framework consisting of two key components: a Gas Computation Mechanism (GCM), which quantifies the load a transaction places on the network in terms of parallelization and computation, measured in units of gas, and a Transaction Fee Mechanism (TFM), which assigns a price to each unit of gas. We additionally introduce a set of desirable properties for a GCM, propose several candidate mechanisms, and evaluate them against these criteria. Our analysis highlights two strong candidates: the weighted area GCM, which integrates smoothly with existing TFMs such as EIP‑1559 and satisfies a broad subset of the outlined properties, and the time-proportional makespan GCM, which assigns gas costs based on the context of the entire block’s schedule and, through this dependence on the overall execution outcome, captures the dynamics of parallel execution more accurately.
Cite as

Bahar Acilan, Andrei Constantinescu, Lioba Heimbach, and Roger Wattenhofer. Transaction Fee Market Design for Parallel Execution. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 23:1-23:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{acilan_et_al:LIPIcs.AFT.2025.23,
  author =	{Acilan, Bahar and Constantinescu, Andrei and Heimbach, Lioba and Wattenhofer, Roger},
  title =	{{Transaction Fee Market Design for Parallel Execution}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{23:1--23:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-400-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{354},
  editor =	{Avarikioti, Zeta and Christin, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2025.23},
  URN =		{urn:nbn:de:0030-drops-247426},
  doi =		{10.4230/LIPIcs.AFT.2025.23},
  annote =	{Keywords: blockchain, transaction fee mechanism, parallel execution}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.2
A Formal Analysis of Algorithms for Matroids and Greedoids

Authors: Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, and Adem Rimpapa

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We present a formal analysis, in Isabelle/HOL, of optimisation algorithms for matroids, which are useful generalisations of combinatorial structures that occur in optimisation, and greedoids, which are a generalisation of matroids. Although some formalisation work has been done earlier on matroids, our work here presents the first formalisation of results on greedoids, and many results we formalise in relation to matroids are also formalised for the first time in this work. We formalise the analysis of a number of optimisation algorithms for matroids and greedoids. We also derive from those algorithms executable implementations of Kruskal’s algorithm for computing optimal spanning trees, an algorithm for maximum cardinality matching for bi-partite graphs, and Prim’s algorithm for computing minimum weight spanning trees.
Cite as

Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, and Adem Rimpapa. A Formal Analysis of Algorithms for Matroids and Greedoids. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 2:1-2:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2025.2,
  author =	{Abdulaziz, Mohammad and Ammer, Thomas and Meenakshisundaram, Shriya and Rimpapa, Adem},
  title =	{{A Formal Analysis of Algorithms for Matroids and Greedoids}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{2:1--2:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.2},
  URN =		{urn:nbn:de:0030-drops-246012},
  doi =		{10.4230/LIPIcs.ITP.2025.2},
  annote =	{Keywords: Matroids, Greedoids, Combinatorial Optimisation, Graph Algorithms, Isabelle/HOL, Formal Verification}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.10
Program Logics for Ledgers

Authors: Orestis Melkonian, Wouter Swierstra, and James Chapman

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant.
Cite as

Orestis Melkonian, Wouter Swierstra, and James Chapman. Program Logics for Ledgers. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{melkonian_et_al:OASIcs.FMBC.2025.10,
  author =	{Melkonian, Orestis and Swierstra, Wouter and Chapman, James},
  title =	{{Program Logics for Ledgers}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{10:1--10:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.10},
  URN =		{urn:nbn:de:0030-drops-230370},
  doi =		{10.4230/OASIcs.FMBC.2025.10},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO separation logic, program semantics, formal verification, Agda}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.19
Decidability and Complexity of Tree Share Formulas

Authors: Xuan Bach Le, Aquinas Hobor, and Anthony W. Lin

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
Fractional share models are used to reason about how multiple actors share ownership of resources. We examine the decidability and complexity of reasoning over the "tree share" model of Dockins et al. using first-order logic, or fragments thereof. We pinpoint a connection between the basic operations on trees union, intersection, and complement and countable atomless Boolean algebras, allowing us to obtain decidability with the precise complexity of both first-order and existential theories over the tree share model with the aforementioned operations. We establish a connection between the multiplication operation on trees and the theory of word equations, allowing us to derive the decidability of its existential theory and the undecidability of its full first-order theory. We prove that the full first-order theory over the model with both the Boolean operations and the restricted multiplication operation (with constants on the right hand side) is decidable via an embedding to tree-automatic structures.
Cite as

Xuan Bach Le, Aquinas Hobor, and Anthony W. Lin. Decidability and Complexity of Tree Share Formulas. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.FSTTCS.2016.19,
  author =	{Le, Xuan Bach and Hobor, Aquinas and Lin, Anthony W.},
  title =	{{Decidability and Complexity of Tree Share Formulas}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.19},
  URN =		{urn:nbn:de:0030-drops-68544},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.19},
  annote =	{Keywords: Fractional Share Models, Resource Accounting, Countable Atomless Boolean Algebras, Word Equations, Tree Automatic Structures}
}
Document
DOI: 10.4230/DagSemProc.10351.3
A Theory of Termination via Indirection

Authors: Robert Dockins and Aquinas Hobor

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract
Step-indexed models provide approximations to a class of domain equations and can prove type safety, partial correctness, and program equivalence; however, a common misconception is that they are inapplicable to liveness problems. We disprove this by applying step-indexing to develop the first Hoare logic of total correctness for a language with function pointers and semantic assertions. In fact, from a liveness perspective, our logic is stronger: we verify explicit time resource bounds. We apply our logic to examples containing nontrivial "higher-order" uses of function pointers and we prove soundness with respect to a standard operational semantics. Our core technique is very compact and may be applicable to other liveness problems. Our results are machine checked in Coq.
Cite as

Robert Dockins and Aquinas Hobor. A Theory of Termination via Indirection. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dockins_et_al:DagSemProc.10351.3,
  author =	{Dockins, Robert and Hobor, Aquinas},
  title =	{{A Theory of Termination via Indirection}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.3},
  URN =		{urn:nbn:de:0030-drops-28050},
  doi =		{10.4230/DagSemProc.10351.3},
  annote =	{Keywords: Step-indexed Models, Termination}
}
  • Refine by Type
  • 5 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2016
  • 1 2010

  • Refine by Author
  • 2 Hobor, Aquinas
  • 1 Abdulaziz, Mohammad
  • 1 Acilan, Bahar
  • 1 Ammer, Thomas
  • 1 Chapman, James
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 1 OASIcs
  • 1 DagSemProc

  • Refine by Classification
  • 1 Applied computing → Economics
  • 1 Theory of computation → Discrete optimization
  • 1 Theory of computation → Invariants
  • 1 Theory of computation → Program semantics
  • 1 Theory of computation → Program verification
  • Show More...

  • Refine by Keyword
  • 2 blockchain
  • 1 Agda
  • 1 Combinatorial Optimisation
  • 1 Countable Atomless Boolean Algebras
  • 1 Formal Verification
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact