Workshop on International Cooperation Program

Theories and Frameworks for Trustworthy Development of Ubiquitous Information Systems Based on Bidirectional Computing

00 Days
00 Hours
00 Minutes
00 Seconds

Introduction

Welcome to the Joint Conference on the International Cooperation Program! This conference aims to bring together leading scholars to engage in in-depth presentations and discussions centered on the project's core objective—leveraging the advanced concept of "bidirectional computing" to construct a comprehensive trusted development framework spanning from formal theories to engineering practices. The symposium is designed to establish a high-level, international academic dialogue platform for discussing cutting-edge issues, sharing interim research findings, and planning future collaborative research directions.

Topics of Interest

Read-Visible Serializability and Scalable Transaction Processing
Towards Translating SQL View Update Statements
Change Managements among Multiple Information Sources using Bidirectional Transformations and Operational Transformations
Static Analysis of BX-based Data Sharing

Date

Mark your calendars for this exciting event:

December 06 - December 09, 2025

Location

The conference will be held at:

Meeting Room 1, Building 1
Zhongguan Xinyuan
Haidian District, Beijing

Program

December 06 (Saturday)

Arrive & Check In

December 07 (Sunday) Morning 9:00-11:40

9:00 - 9:10: Zhenjiang Hu (PKU), Opening Remarks and Introduction

Session 1 (Host: Zhenjiang Hu)

9:10 - 9:40: Makoto Onizuka (The University of Osaka), Read-Visible Serializability and Scalable Transaction Processing
Abstract: We propose Read-Visible Serializability (RVSR), a generalized transactional semantics unifying CRDT/OT reconciliation with database-level guarantees for user-visible reads. Unlike CSR or VSR, RVSR only requires each visible read to reflect a serial prefix of a total order over effects under a deterministic reconciliation policy ρ. We formalize RVSR, place it in the hierarchy CSR ⊂ VSR ⊂ RVSR ⊂ FSR, and prove an equivalent ρ-based characterization. Using return-value commutativity (RVC), we derive a sufficient condition for merged-state equivalence and provide an SMT-based RVC checker. We implement these semantics in Auto-CRDT Planner, which compiles SQL to an effects IR and automatically selects (i) CRDT rewriting, (ii) key-local coordination for ordered updates, or (iii) serializable fallback. On TPC-C workloads, Auto achieves much higher throughput than 2PL while preserving correctness through PN-counters, escrow-based decrements, and merge-then-read snapshots. RVSR thus offers a principled foundation for safe, scalable reconciliation across transactional and CRDT systems.
9:40 - 10:10: Hiroyuki Kato (NII), Towards Translating SQL View Update Statements
Abstract: The view update problem is a long-standing challenge in database research: how can updates applied to database views be correctly translated into corresponding updates on the underlying base relations? This problem is complicated by the fact that multiple possible base updates may correspond to a single view modification. Recent work has approached this challenge using bidirectional transformation (BX) techniques, a framework that has been extensively studied in the programming languages community. BX offers a rigorous foundation by ensuring well-behavedness (i.e., side-effect-freeness) of updates. However, applying BX principles directly to practical database systems remains a nontrivial task. A key difficulty lies in a fundamental assumption of BX—that updates are performed on free-standing views, which are independent, in-memory structures rather than persistent database objects. In contrast, real-world database applications interact with views just as they do with base tables, typically without distinguishing between them. Since data modifications in relational systems are carried out via standard SQL statements (e.g., INSERT, DELETE, UPDATE), achieving updatable views through these same mechanisms is essential for practical deployment. In this talk, I will present our ongoing work towards translating SQL view update statements in a way that preserves well-behavedness, aiming to bridge the gap between theoretical BX frameworks and practical database implementations.
10:10 - 10:40: Coffee Break
10:40 - 11:10: From PKU Speaker, Updating
Abstract: Updating.
11:10 - 11:40: From PKU Speaker, Updating
Abstract: Updating.

December 07 (Sunday) Afternoon 14:00-16:30

Session 2 (Host: Zhenjiang Hu)

14:00 - 14:30: Soichiro Hidaka (The University of Osaka), Change Managements among Multiple Information Sources using Bidirectional Transformations and Operational Transformations
Abstract: Multidirectional transformations maintain consistency among more than two information sources. They are expected to play an important role in collaborative data sharing. Bidirectional transformations have been applied for such scenario by architectures such as Dejima and BCDS. Assuming Dejima architecture as bipartite network of bidirectional transformations in which base tables and views constitute two sets of nodes while bidirectional transformations correspond to the edges between base tables and views, we have developed an evolutionary framework to cope with various reconfigurations such as joining of new nodes and reconciliation among bidirectional transformations having different ranges while incoming common nodes. Although such framework seems promising, we still have challenges such as reconciliation of conflicting updates in such nodes. We could approach this problem by operational transformations to merge such updates. However, since the resultant state after the merging is different in general from the result of applying any one of these update only. That causes weakening of synchronization property even if each component bidirectional transformation satisfy strong round-tripping property called PutGet. In this presentation, we recap the evolutionary framework and briefly discuss the challenges related to the conflict resolution problem. We also would like to introduce some of the efforts related to change managements in the Infrastructure Software Laboratory led by the presenter in Hosei University.
14:30 - 15:00: Yasunori Ishihara (The University of Osaka), Static Analysis of BX-based Data Sharing
Abstract: This presentation discusses two topics related to the static analysis of BX-based data sharing. The first topic is consistency checking of a given BX (more specifically, a given putback function) for relational data against given functional dependencies. Assuming that the get function corresponds to a SPJ (select-project-join) query, we focus on two types of putback functions, namely, "less-source-change put" and "least-source-size put." Then, we show decidable necessary and sufficient conditions for a given putback function to never violate given functional dependencies of the source schema. The second topic is confidentiality checking of the Dejima architecture, which was proposed by the BISCUITS project. We first define confidentiality on the Dejima architecture, and then discuss the conditions under which this confidentiality property is decidable.
15:00 - 15:30: Coffee Break
15:30 - 16:00: From PKU Speaker, Updating
Abstract: Updating.
16:00 - 16:30: From PKU Speaker, Updating
Abstract: Updating.

December 08 (Monday) Morning: 09:00 - 11:00

Session 3 (Host: Zhenjiang Hu)

09:00 - 11:00: Project communication

December 08 (Monday) Afternoon: 14:00 - 17:00

Session 4(Host: Zhenjiang Hu)

Free discussion

December 09 (Tuesday)

Leave

Meals

Midday Meal on December 07 & 08

Zhongguan Xinyuan
Haidian District, Beijing

Evening Meal on December 07 & 08

yi yuan
Haidian District, Beijing

Attendees

Committee (Alphabetical Order)

Contact

For inquiries, please contact us at:

yecui at pku.edu.cn
wangjianjia at pku.edu.cn