报告1：Formalising Resilient Distributed Systems in Lean 4: Local Checkpoints, Byzantine Faults, and Three Routes to Provably Safe Recovery

报告时间：7月20日09：30-10：40

报告地点：理科大楼B211

报告摘要：

What does it mean, precisely, for a distributed system to survive a crash? A folklore answer says: resume from a snapshot taken before the failure and carry on safely. This talk presents a fully mechanised Lean 4 development that turns this folklore into theorems, for systems where checkpoints are strictly local, communication is asynchronous, and up to f nodes are Byzantine.

The starting point is a cautionary observation: the natural sufficient conditions imply that crashes never happen, making the recovery property vacuously true. The interesting theory lives strictly between "crashes impossible" and "crashes unrecoverable," and we explore it along three routes. First, viability kernels, greatest fixed points on the lattice of state predicates, yield the weakest checkpointing policy for safe, crash-free continuations, with both sufficiency and necessity mechanised; checkpointing becomes controller synthesis. Second, weak bisimulation (via the CSLib library) recasts resilience behaviourally: under a write-ahead snapshot discipline, a crashed node is provably indistinguishable from the protocol that never failed, its checkpointis its behaviour. Third, self-certifying snapshots carry quorum evidence, inverting the fault model, a crash is a failed local audit, with the classical N ≥ 3f + 1 threshold mechanised in Mathlib's finite combinatorics.

报告人简介：

Dr. Boris Düdder is an associate professor of software engineering and formal methods at the Department of Computer Science (DIKU) at the University of Copenhagen (UCPH). He is the Deputy Head of Department for Teaching at DIKU, the Director of the Trustworthy AI Lab at UCPH, and a member of the working group on the General-Purpose AI Code of Practice at DG CNECT, the European Commission.  He is widely recognised as a leading authority in the field of software engineering and formal methods. Dr. Düdder leads the research group on Software Engineering & Formal Methods at DIKU. His primary research interests lie in the areas of formal methods and programming languages in software engineering of trustworthy distributed systems, with a focus on automated program generation for adaptive systems with high-reliability guarantees. His work also involves the computational foundations of reliable and secure Big Data ecosystems. Dr. Düdder’s long-term research vision is to develop dependable, adaptive, and software-defined technical systems based on program synthesis for manufacturing, healthcare, and logistics.

报告2：Transactional Cloud Applications: Status Quo, Challenges, and Opportunities

报告时间：7月20日10：40-11：30

报告地点：理科大楼B211

报告摘要：

Transactional cloud applications such as payment, booking, reservation systems, and complex business workflows are currently being rewritten for deployment in the cloud. This migration to the cloud is happening mainly for reasons of cost and scalability. Over the years, application developers have used different migration approaches, such as microservice frameworks, actors, and stateful dataflow systems.

The migration to the cloud has brought back data management challenges traditionally handled by database management systems. Those challenges include ensuring state consistency, maintaining durability, and managing the application lifecycle. At the same time, the shift to a distributed computing infrastructure introduced new issues, such as message delivery, task scheduling, containerization, and (auto)scaling

Although the data management community has made progress in developing analytical and transactional database systems, transactional cloud applications have received little attention in database research. This tutorial aims to highlight recent trends in the area and discusses open research challenges for the data management community.

报告人简介：

Yongluan Zhou is Professor in the Department of Computer Science (DIKU) at the University of Copenhagen, where he leads the Data Management Systems Lab (DMS Lab). He also heads the MSc in Computer Science at DIKU. Prior to his current position, he worked as an Associate Professor at the University of Southern Denmark (SDU) and as a postdoc at the Ecole Polytechnique Fédérale de Lausanne (EPFL). He earned his Ph.D. in Computer Science from the National University of Singapore (NUS). His research interests span database systems and distributed systems, with his recent focus being on scalable event-driven systems. He has authored more than 80 peer-reviewed research articles in international journals and conference proceedings. He serves on the EDBT Executive Board and the SSDBM Steering Committee and has chaired various international conferences, including DEBS 2022, SSDBM 2022, and EDBT 2020. He has also served on the Program Committees of many other international conferences, including SIGMOD, VLDB, ICDE, EDBT.

报告3：Key Technologies for Secure and Scalable Sharding Blockchain Consensus

报告时间：7月20日14：00-14：50

报告地点：理科大楼B211

报告摘要：

Blockchain sharding is a promising approach to improving blockchain scalability by enabling parallel transaction processing across multiple shards. However, achieving both high performance and strong security remains a fundamental challenge, particularly in the presence of frequent cross-shard transactions and potential shard corruption.

To address the efficiency bottleneck of cross-shard transaction processing, Kronos introduces a secure and generic sharding blockchain consensus framework that reduces cross-shard transaction processing overhead. By introducing a buffer-based cross-shard consensus pattern and a lightweight certification mechanism, Kronos achieves efficient and atomic cross-shard transaction processing even in asynchronous network settings. To further improve the robustness of sharding blockchains against corrupted shards, Camael enables corrupted-shard tolerance. Through efficient mechanisms for handling liveness and safety violations, Camael preserves system consistency and ensures efficient transaction processing even when individual shards are corrupted. Together, these techniques significantly enhance the scalability, efficiency, and robustness of sharding blockchains, providing practical foundations for next-generation secure and scalable blockchain systems.

报告人简介：

Yizhong Liu is an Associate Professor and Ph.D. Supervisor at the School of Cyber Science and Technology, Beihang University. He was selected for the Young Elite Scientists Sponsorship Program by the China Association for Science and Technology (CAST) through the Chinese Institute of Electronics, and received the Outstanding Doctoral Dissertation Award from the Chinese Institute of Command and Control (CICC). His research interests include blockchain, cryptography, artificial intelligence security, and privacy-preserving computation. He has published over 60 academic papers, including over 40 papers as the first or corresponding author. More than 20 papers have appeared in top-tier CCF-A conferences and journals, including ACM CCS, IEEE S&P, USENIX Security, NDSS, ACM WWW, IEEE TDSC, IEEE TIFS, and IEEE JSAC. He has also authored one Springer monograph. His research contributions have been recognized with awards including the First Prize of Science and Technology Progress Award from the Chinese Institute of Command and Control, the Outstanding Innovation Achievement Award in Cybersecurity, and the First Prize in the China Internet Security Competition.