Ziyi Guan, Jason Chun Lok Li, Zhijian Hou, Pingping Zhang, Donglai Xu, Yuzhi Zhao, Mengyang Wu, Jinpeng Chen, Thanh-Toan Nguyen, Pengfei Xian, Wenao Ma, Shengchao Qin, Graziano Chesi, Ngai Wong. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing. 2025.

This paper presents a systematic and comprehensive survey on blockchain interoperability, where interoperability is defined as the ability of blockchains to flexibly transfer assets, share data, and invoke smart contracts across a mix of public, private, and consortium blockchains without any changes to the underlying blockchain systems. Analyzing the vast landscape of both research papers and industry projects, we classify the existing works into five categories, namely, (1) sidechains, (2) notary schemes, (3) hashed time lock contracts (HTLC), (4) relays, and (5) blockchain agnostic protocols. We analyze the existing works under a taxonomy that consists of system and safety characteristics, such as decentralization, direction of communication, locking mechanism, verification mechanism, trust, safety, liveness, and atomicity. Different from other surveys, we are the first to evaluate the performance of some representative interoperability approaches between Bitcoin and Ethereum covering sidechains, notary schemes, and HTLCs. Even though the performance of cross-chain transactions is low (typically fewer than 10 transactions per second), the main reason is the underlying blockchain (e.g., Bitcoin and Ethereum) and not the interoperability approach. Finally, we discuss existing challenges and possible research directions in blockchain interoperability. For example, we identify challenges in interoperability across permissioned and permissionless blockchains, in interacting with scripting blockchains, in security and privacy.

SL-COMP aims at bringing together researchers interested on improving the state of the art of the automated deduction methods for Separation Logic (SL). The event took place twice until now and collected more than 1K problems for different fragments of SL. The input format of problems is based on the SMT-LIB format and therefore fully typed; only one new command is added to SMT-LIB’s list, the command for the declaration of the heap’s type. The SMT-LIB theory of SL comes with ten logics, some of them being combinations of SL with linear arithmetics. The competition’s divisions are defined by the logic fragment, the kind of decision problem (satisfiability or entailment) and the presence of quantifiers. Until now, SL-COMP has been run on the StarExec platform, where the benchmark set and the binaries of participant solvers are freely available. The benchmark set is also available with the competition’s documentation on a public repository in GitHub.