10 Search Results for "Sun, Xinyuan"

Document
DOI: 10.4230/LIPIcs.SoCG.2026.78
Mapping Chemical Space: Topological Data Analysis of Chemical Latent Space with Mapper

Authors: Dhruv Meduri, Chuan-Shen Hu, Cong Shen, Kelin Xia, and Bei Wang

Published in: LIPIcs, Volume 367, 42nd International Symposium on Computational Geometry (SoCG 2026)

Abstract
The vast chemical space, encompassing virtually innumerable molecules and materials, presents both immense opportunities and significant challenges. The design and discovery of novel drugs and functional materials may be viewed as a search within this space; however, the sheer scale of potential candidates renders exhaustive exploration infeasible. To address this, we introduce Chemical Mapper, a framework that integrates topological data analysis with deep learning to enable the visual exploration and analysis of chemical latent spaces. At its core, Chemical Mapper employs mapper, a widely used tool in topological data analysis, to investigate the organizational principles of chemical latent spaces defined by molecular representations learned by geometric deep learning models. In doing so, Chemical Mapper not only highlights groups of molecular representations but also uncovers the relationships among them through linkages and branching structures. Our results show that Chemical Mapper reveals intrinsic patterns associated with molecular scaffolds, functional groups, and chemical properties, as well as the structural and functional evolutions of the molecules.
Cite as

Dhruv Meduri, Chuan-Shen Hu, Cong Shen, Kelin Xia, and Bei Wang. Mapping Chemical Space: Topological Data Analysis of Chemical Latent Space with Mapper. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 78:1-78:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{meduri_et_al:LIPIcs.SoCG.2026.78,
  author =	{Meduri, Dhruv and Hu, Chuan-Shen and Shen, Cong and Xia, Kelin and Wang, Bei},
  title =	{{Mapping Chemical Space: Topological Data Analysis of Chemical Latent Space with Mapper}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{78:1--78:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-418-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{367},
  editor =	{Ahn, Hee-Kap and Hoffmann, Michael and Nayyeri, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2026.78},
  URN =		{urn:nbn:de:0030-drops-258854},
  doi =		{10.4230/LIPIcs.SoCG.2026.78},
  annote =	{Keywords: Practice of computational topology, topological data analysis, applications in chemistry, mapper algorithm, high-dimensional data analysis, chemical spaces, geometric deep learning, latent space geometry}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.59
On Approximating the f-Divergence Between Two Ising Models

Authors: Weiming Feng and Yucheng Fu

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
The f-divergence is a fundamental notion that measures the difference between two distributions. In this paper, we study the problem of approximating the f-divergence between two Ising models, which is a generalization of recent work on approximating the TV-distance. Given two Ising models ν and μ, which are specified by their interaction matrices and external fields, the problem is to approximate the f-divergence D_f (ν ‖ μ) within an arbitrary relative error e^{±ε}. For χ^α-divergence with a constant integer α, we establish both algorithmic and hardness results. The algorithm works in a parameter regime that matches the hardness result. Our algorithm can be extended to other f-divergences such as α-divergence, Kullback-Leibler divergence, Rényi divergence, Jensen-Shannon divergence, and squared Hellinger distance.
Cite as

Weiming Feng and Yucheng Fu. On Approximating the f-Divergence Between Two Ising Models. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 59:1-59:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{feng_et_al:LIPIcs.ITCS.2026.59,
  author =	{Feng, Weiming and Fu, Yucheng},
  title =	{{On Approximating the f-Divergence Between Two Ising Models}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{59:1--59:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.59},
  URN =		{urn:nbn:de:0030-drops-253469},
  doi =		{10.4230/LIPIcs.ITCS.2026.59},
  annote =	{Keywords: Ising model, f-divergence, approximation algorithms, randomized algorithms}
}
Document
DOI: 10.4230/LIPIcs.AFT.2025.7
Mechanism Design for Automated Market Makers

Authors: T-H. Hubert Chan, Ke Wu, and Elaine Shi

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

Abstract
Blockchains have popularized automated market makers (AMMs), applications that run on a blockchain, maintain a pool of crypto-assets, and execute trades with users governed by some pricing function. AMMs have also introduced a significant challenge known as the Miner Extractable Value (MEV). Specifically, miners who control the contents and sequencing of transactions in a block can extract value by front-running and back-running users' transactions, creating arbitrage opportunities that guarantee them risk-free returns. MEV not only harms ordinary users, but more critically, encourages miners to auction off favorable transaction placements to users and arbitragers. This has fostered a more centralized off-chain eco-system, departing from the decentralized equilibrium originally envisioned for the blockchain infrastructure layer. In this paper, we consider how to design AMM mechanisms that eliminate MEV opportunities. Specifically, we propose a new AMM mechanism that processes all transactions contained within a block according to some pre-defined rules, ensuring that some constant potential function is maintained after processing the batch. We show that our new mechanism satisfies two tiers of guarantees. First, for legacy blockchains where each block is proposed by a single (possibly rotating) miner, we prove that our mechanism satisfies arbitrage resilience, i.e., a miner cannot gain risk-free profit. Second, for blockchains where the block proposal process is decentralized and offers sequencing-fairness, we prove a strictly stronger notion called strategy proofness - roughly speaking, we guarantee that any individual user’s best response is to follow the honest strategy. Our results complement prior works on MEV resilience in the following senses. First, prior works have shown impossibilities to address MEV entirely at the consensus level. Our work demonstrates a new paradigm of mechanism design at the application (i.e., smart contract) layer to ensure provable guarantees of strategy proofness. Second, many works have attempted to augment the underlying consensus protocol with extra properties such as sequencing fairness. While most previous works heuristically argued why these extra properties help to mitigate MEV, our work demonstrates in a mathematically formal manner how to leverage such consensus-level properties to aid the design of strategy-proof mechanisms.
Cite as

T-H. Hubert Chan, Ke Wu, and Elaine Shi. Mechanism Design for Automated Market Makers. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chan_et_al:LIPIcs.AFT.2025.7,
  author =	{Chan, T-H. Hubert and Wu, Ke and Shi, Elaine},
  title =	{{Mechanism Design for Automated Market Makers}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{7:1--7:22},
  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.7},
  URN =		{urn:nbn:de:0030-drops-247265},
  doi =		{10.4230/LIPIcs.AFT.2025.7},
  annote =	{Keywords: Mechanism design, game theory, strategy proof, blockchain}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.46
Efficient Parallel Ising Samplers via Localization Schemes

Authors: Xiaoyu Chen, Hongyang Liu, Yitong Yin, and Xinyuan Zhang

Published in: LIPIcs, Volume 353, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)

Abstract
We introduce efficient parallel algorithms for sampling from the Gibbs distribution and estimating the partition function of Ising models. These algorithms achieve parallel efficiency, with polylogarithmic depth and polynomial total work, and are applicable to Ising models in the following regimes: (1) Ferromagnetic Ising models with external fields; (2) Ising models with interaction matrix J of operator norm ‖J‖₂ < 1. Our parallel Gibbs sampling approaches are based on localization schemes, which have proven highly effective in establishing rapid mixing of Gibbs sampling. In this work, we employ two such localization schemes to obtain efficient parallel Ising samplers: the field dynamics induced by negative-field localization, and restricted Gaussian dynamics induced by stochastic localization. This shows that localization schemes are powerful tools, not only for achieving rapid mixing but also for the efficient parallelization of Gibbs sampling.
Cite as

Xiaoyu Chen, Hongyang Liu, Yitong Yin, and Xinyuan Zhang. Efficient Parallel Ising Samplers via Localization Schemes. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 46:1-46:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.APPROX/RANDOM.2025.46,
  author =	{Chen, Xiaoyu and Liu, Hongyang and Yin, Yitong and Zhang, Xinyuan},
  title =	{{Efficient Parallel Ising Samplers via Localization Schemes}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{46:1--46:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.46},
  URN =		{urn:nbn:de:0030-drops-244129},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.46},
  annote =	{Keywords: Localization scheme, parallel sampling, Ising model}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.51
Improved Mixing of Critical Hardcore Model

Authors: Zongchen Chen and Tianhui Jiang

Published in: LIPIcs, Volume 353, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)

Abstract
The hardcore model is one of the most classic and widely studied examples of undirected graphical models. Given a graph G, the hardcore model describes a Gibbs distribution of λ-weighted independent sets of G. In the last two decades, a beautiful computational phase transition has been established at a precise threshold λ_c(Δ) where Δ denotes the maximum degree, where the task of sampling independent sets transitions from polynomial-time solvable to computationally intractable. We study the critical hardcore model where λ = λ_c(Δ) and show that the Glauber dynamics, a simple yet popular Markov chain algorithm, mixes in Õ(n^{7.44 + O(1/Δ)}) time on any n-vertex graph of maximum degree Δ ≥ 3, significantly improving the previous upper bound Õ(n^{12.88 + O(1/Δ)}) by the recent work [Chen et al., 2024]. The core property we establish in this work is that the critical hardcore model is O(√n)-spectrally independent, improving the trivial bound of n and matching the critical behavior of the Ising model. Our proof approach utilizes an online decision-making framework to study a site percolation model on the infinite (Δ-1)-ary tree, which can be interesting by itself.
Cite as

Zongchen Chen and Tianhui Jiang. Improved Mixing of Critical Hardcore Model. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 51:1-51:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.APPROX/RANDOM.2025.51,
  author =	{Chen, Zongchen and Jiang, Tianhui},
  title =	{{Improved Mixing of Critical Hardcore Model}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{51:1--51:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.51},
  URN =		{urn:nbn:de:0030-drops-244176},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.51},
  annote =	{Keywords: Hardcore model, Phase transition, Glauber dynamics, Spectral independence, Online decision making, Site percolation}
}
Document
Survey
DOI: 10.4230/TGDK.3.1.3
Uncertainty Management in the Construction of Knowledge Graphs: A Survey

Authors: Lucas Jarnac, Yoan Chabot, and Miguel Couceiro

Published in: TGDK, Volume 3, Issue 1 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 1

Abstract
Knowledge Graphs (KGs) are a major asset for companies thanks to their great flexibility in data representation and their numerous applications, e.g., vocabulary sharing, Q&A or recommendation systems. To build a KG, it is a common practice to rely on automatic methods for extracting knowledge from various heterogeneous sources. However, in a noisy and uncertain world, knowledge may not be reliable and conflicts between data sources may occur. Integrating unreliable data would directly impact the use of the KG, therefore such conflicts must be resolved. This could be done manually by selecting the best data to integrate. This first approach is highly accurate, but costly and time-consuming. That is why recent efforts focus on automatic approaches, which represent a challenging task since it requires handling the uncertainty of extracted knowledge throughout its integration into the KG. We survey state-of-the-art approaches in this direction and present constructions of both open and enterprise KGs. We then describe different knowledge extraction methods and discuss downstream tasks after knowledge acquisition, including KG completion using embedding models, knowledge alignment, and knowledge fusion in order to address the problem of knowledge uncertainty in KG construction. We conclude with a discussion on the remaining challenges and perspectives when constructing a KG taking into account uncertainty.
Cite as

Lucas Jarnac, Yoan Chabot, and Miguel Couceiro. Uncertainty Management in the Construction of Knowledge Graphs: A Survey. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 1, pp. 3:1-3:48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{jarnac_et_al:TGDK.3.1.3,
  author =	{Jarnac, Lucas and Chabot, Yoan and Couceiro, Miguel},
  title =	{{Uncertainty Management in the Construction of Knowledge Graphs: A Survey}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{3:1--3:48},
  ISSN =	{2942-7517},
  year =	{2025},
  volume =	{3},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.1.3},
  URN =		{urn:nbn:de:0030-drops-233733},
  doi =		{10.4230/TGDK.3.1.3},
  annote =	{Keywords: Knowledge reconciliation, Uncertainty, Heterogeneous sources, Knowledge graph construction}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.3
Formal Verification in Solidity and Move: Insights from a Comparative Analysis

Authors: Massimo Bartoletti, Silvia Crafa, and Enrico Lipparini

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

Abstract
Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or to guarantee their absence, as well as checking whether the business logic is correctly implemented. For Solidity, even though there already exist several mature verification tools, the semantical quirks of the language can make verification quite hard in practice. Move, on the other hand, has been designed with security and verification in mind, and it has been accompanied since its early stages by a formal verification tool, the Move Prover. In this paper, we investigate through a comparative analysis: 1) how the different designs of the two contract languages impact verification, and 2) what is the state-of-the-art of verification tools for the two languages, and how do they compare on three paradigmatic use cases. Our investigation is supported by an open dataset of verification tasks performed in Certora and in the Aptos Move Prover.
Cite as

Massimo Bartoletti, Silvia Crafa, and Enrico Lipparini. Formal Verification in Solidity and Move: Insights from a Comparative Analysis. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bartoletti_et_al:OASIcs.FMBC.2025.3,
  author =	{Bartoletti, Massimo and Crafa, Silvia and Lipparini, Enrico},
  title =	{{Formal Verification in Solidity and Move: Insights from a Comparative Analysis}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{3:1--3:18},
  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.3},
  URN =		{urn:nbn:de:0030-drops-230302},
  doi =		{10.4230/OASIcs.FMBC.2025.3},
  annote =	{Keywords: Smart contracts, Solidity, Move, Verification, Blockchain}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.8
Formal Verification of a Fail-Safe Cross-Chain Bridge

Authors: Filip Marić, Bernhard Scholz, and Pavle Subotić

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

Abstract
Cross-chain bridges are financial services that interconnect blockchains. High monetary values flow through these bridges, and their security must be safeguarded. However, designing real-world cross-chain bridges is a difficult endeavor. Due to blockchain’s closed-world nature, tokens cannot be transferred from a sender to a receiver chain; on the contrary, they need complex logic that maintains an equilibrium on both chains, even if either the chains or the bridge fail. This paper formally verifies a model of a novel fail-safe cross-chain bridge to ensure correctness. We define formal requirements and prove the bridge is safe using the Isabelle/HOL proof assistant.
Cite as

Filip Marić, Bernhard Scholz, and Pavle Subotić. Formal Verification of a Fail-Safe Cross-Chain Bridge. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{maric_et_al:OASIcs.FMBC.2025.8,
  author =	{Mari\'{c}, Filip and Scholz, Bernhard and Suboti\'{c}, Pavle},
  title =	{{Formal Verification of a Fail-Safe Cross-Chain Bridge}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{8:1--8:18},
  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.8},
  URN =		{urn:nbn:de:0030-drops-230342},
  doi =		{10.4230/OASIcs.FMBC.2025.8},
  annote =	{Keywords: Cross-Chain Bridge, Formal Verification, Logic, Security}
}
Document
Survey
DOI: 10.4230/TGDK.1.1.4
Knowledge Graph Embeddings: Open Challenges and Opportunities

Authors: Russa Biswas, Lucie-Aimée Kaffee, Michael Cochez, Stefania Dumbrava, Theis E. Jendal, Matteo Lissandrini, Vanessa Lopez, Eneldo Loza Mencía, Heiko Paulheim, Harald Sack, Edlira Kalemi Vakaj, and Gerard de Melo

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
While Knowledge Graphs (KGs) have long been used as valuable sources of structured knowledge, in recent years, KG embeddings have become a popular way of deriving numeric vector representations from them, for instance, to support knowledge graph completion and similarity search. This study surveys advances as well as open challenges and opportunities in this area. For instance, the most prominent embedding models focus primarily on structural information. However, there has been notable progress in incorporating further aspects, such as semantics, multi-modal, temporal, and multilingual features. Most embedding techniques are assessed using human-curated benchmark datasets for the task of link prediction, neglecting other important real-world KG applications. Many approaches assume a static knowledge graph and are unable to account for dynamic changes. Additionally, KG embeddings may encode data biases and lack interpretability. Overall, this study provides an overview of promising research avenues to learn improved KG embeddings that can address a more diverse range of use cases.
Cite as

Russa Biswas, Lucie-Aimée Kaffee, Michael Cochez, Stefania Dumbrava, Theis E. Jendal, Matteo Lissandrini, Vanessa Lopez, Eneldo Loza Mencía, Heiko Paulheim, Harald Sack, Edlira Kalemi Vakaj, and Gerard de Melo. Knowledge Graph Embeddings: Open Challenges and Opportunities. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 4:1-4:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{biswas_et_al:TGDK.1.1.4,
  author =	{Biswas, Russa and Kaffee, Lucie-Aim\'{e}e and Cochez, Michael and Dumbrava, Stefania and Jendal, Theis E. and Lissandrini, Matteo and Lopez, Vanessa and Menc{\'\i}a, Eneldo Loza and Paulheim, Heiko and Sack, Harald and Vakaj, Edlira Kalemi and de Melo, Gerard},
  title =	{{Knowledge Graph Embeddings: Open Challenges and Opportunities}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:32},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.4},
  URN =		{urn:nbn:de:0030-drops-194783},
  doi =		{10.4230/TGDK.1.1.4},
  annote =	{Keywords: Knowledge Graphs, KG embeddings, Link prediction, KG applications}
}
Document
DOI: 10.4230/OASIcs.FMBC.2021.1
Towards Verified Price Oracles for Decentralized Exchange Protocols

Authors: Kinnari Dave, Vilhelm Sjöberg, and Xinyuan Sun

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)

Abstract
Various smart contracts have been designed and deployed on blockchain platforms to enable cryptocurrency trading, leading to an ever expanding user base of decentralized exchange platforms (DEXs). Automated Market Maker contracts enable token exchange without the need of third party book-keeping. These contracts also serve as price oracles for other contracts, by using a mathematical formula to calculate token exchange rates based on token reserves. However, the price oracle mechanism is vulnerable to attacks both from programming errors and from mistakes in the financial model, and so far their complexity makes it difficult to formally verify them. We present a verified AMM contract and validate its financial model by proving a theorem about a lower bound on the cost of manipulation of the token prices to the attacker. The contract is implemented using the DeepSEA system, which ensures that the theorem applies to the actual EVM bytecode of the contract. This theorem could be used as proof of correctness for other contracts using the AMM, so this is a step towards a verified DeFi landscape.
Cite as

Kinnari Dave, Vilhelm Sjöberg, and Xinyuan Sun. Towards Verified Price Oracles for Decentralized Exchange Protocols. In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dave_et_al:OASIcs.FMBC.2021.1,
  author =	{Dave, Kinnari and Sj\"{o}berg, Vilhelm and Sun, Xinyuan},
  title =	{{Towards Verified Price Oracles for Decentralized Exchange Protocols}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{1:1--1:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.1},
  URN =		{urn:nbn:de:0030-drops-154254},
  doi =		{10.4230/OASIcs.FMBC.2021.1},
  annote =	{Keywords: Smart Contract Verification, Interactive Theorem Proving, Blockchain, Decentralized Finance}
}
  • Refine by Type
  • 10 Document/PDF
  • 9 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 6 2025
  • 1 2023
  • 1 2021

  • Refine by Author
  • 1 Bartoletti, Massimo
  • 1 Biswas, Russa
  • 1 Chabot, Yoan
  • 1 Chan, T-H. Hubert
  • 1 Chen, Xiaoyu
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs
  • 3 OASIcs
  • 2 TGDK

  • Refine by Classification
  • 2 Software and its engineering → Software verification
  • 2 Theory of computation → Random walks and Markov chains
  • 1 Applied computing → Chemistry
  • 1 Computing methodologies → Machine learning approaches
  • 1 Computing methodologies → Semantic networks
  • Show More...

  • Refine by Keyword
  • 2 Blockchain
  • 2 Ising model
  • 1 Cross-Chain Bridge
  • 1 Decentralized Finance
  • 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