Compositional Design, Implementation, and Verification of Swarms
This program is tentative and subject to change.
Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.
This program is tentative and subject to change.
Wed 1 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:30 | Pointers & Distributed SystemsTechnical Papers at I.2.03 Chair(s): Sophia Drossopoulou Imperial College London | ||
14:00 22mTalk | Beyond k-Limiting: Pointer-Flow-Guided Context Sensitivity for Scalable and Precise Rust Pointer Analysis Technical Papers | ||
14:22 22mTalk | Ownership Refinement Types for Pointer Arithmetic and Nested Arrays Technical Papers Yusuke Fujiwara Kyoto University, Japan, Yusuke Matsushita Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University | ||
14:45 22mTalk | Compositional Design, Implementation, and Verification of Swarms Technical Papers Florian Furbach Technical University of Denmark, Lucas Clorius DTU Compute, Roland Kuhn RKSW UG, Hernan Melgratti University of Buenos Aires, Argentina, Alceste Scalas Technical University of Denmark, Emilio Tuosto Gran Sasso Science Institute, L'Aquila, Italy | ||