|
Published: 21st August 2023 DOI: 10.4204/EPTCS.383 ISSN: 2075-2180 |
| Preface Clément Aubert, Cinzia Di Giusto, Simon Fowler and Larisa Safina | |
| Invited Presentation: Techniques for Safe and Highly Available Cloud Applications Carla Ferreira | |
| Invited Presentation: If At First You Don't Succeed: Extended Monitorability through Multiple Executions Adrian Francalanza | |
| Proofs about Network Communication: For Humans and Machines Wolfgang Jeltsch and Javier Díaz | 1 |
| Partially Typed Multiparty Sessions Franco Barbanera and Mariangiola Dezani-Ciancaglini | 15 |
| Algebraic Reasoning About Timeliness Seyed Hossein Haeri, Peter W. Thompson, Peter Van Roy, Magne Haveraaen, Neil J. Davies, Mikhail Barash, Kevin Hammond and James Chapman | 35 |
| On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues Manel Barkallah and Jean-Marie Jacquet | 55 |
| Research Challenges in Orchestration Synthesis Davide Basile and Maurice H. ter Beek | 73 |
This volume contains the proceedings of ICE'23, the 16th Interaction and Concurrency Experience, which was held in Lisbon, Portugal as a satellite event of DisCoTec'23. The previous editions of ICE were affiliated with ICALP'08 (Reykjavik, Iceland), CONCUR'09 (Bologna, Italy), DisCoTec'10 (Amsterdam, The Netherlands), DisCoTec'11 (Reykjavik, Iceland), DisCoTec'12 (Stockholm, Sweden), DisCoTec'13 (Florence, Italy), DisCoTec'14 (Berlin, Germany), DisCoTec'15 (Grenoble, France), DisCoTec'16 (Heraklion, Greece), DisCoTec'17 (Neuchâtel, Switzerland), DisCoTec'18 (Madrid, Spain), DisCoTec'19 (Lyngby, Denmark), DisCoTec'20 (virtual, hosted by the University of Malta), DisCoTec'21 (virtual, hosted by the University of Malta), and DisCoTec'22 (hybrid event, hosted in Lucca, Italy).
The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. This year these interactions took place on the OpenReview platform which combines paper selection features with forum-like interactions. As in the past editions, the forum discussion during the review and selection phase of ICE'23 considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. The time and effort spent on the interaction between reviewers and authors is rewarding for all parties. The discussions on OpenReview make it possible to resolve misunderstandings at an early stage of the review process, to discover and correct mistakes in key definitions, and to improve examples and presentation.
The 2023 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Research papers were blinded for submission, with authors' names and identifying details removed, and authors were given anonymous access to a dedicated section of OpenReview. Each paper was reviewed by three PC members (except for one single oral communication, reviewed by two PC members), and altogether 5 papers were accepted for publication − plus 4 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Carla Ferreira and Adrian Francalanza. The abstracts of these talks are included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop.
We would like to thank the authors of all the submitted papers for their interest in the workshop. We thank Carla Ferreira and Adrian Francalanza for accepting our invitations to present their recent work. We are grateful for the efforts of the PC members:
★ The ICE 2023 Outstanding PC Member Award was awarded this year to Sergueï Lenglet!
Previously, were awarded:
We thank the ICE steering committee and the DisCoTec'23 organizers, in particular the general and workshop chairs (Carla Ferreira and Simão Melo de Sousa, respectively), for providing an excellent environment for the preparation and staging of the event. Finally, we thank the editors of EPTCS for the publication of these post-proceedings and acknowledge the generous support of EAPLS through its support for workshops initiative.
Cloud applications provide increasingly complex services on a global scale. To achieve the quality of service demanded by users, a common technique is to maintain copies of the application's shared data across geographically dispersed locations closer to end users. To this end, it has become increasingly popular to develop applications that rely on weak consistency models where operations requested by a client are executed locally without any coordination with other replicas and immediately returned to the client. These operations are later propagated in the background, leading to different replicas' execution orders and, potentially, divergent replica states. Replicated Data Types (RDTs) that resemble sequential data types (e.g. sets, maps) guarantee convergence by design by providing efficient and deterministic data reconciliation solutions. However, designing new RDTs is challenging. In fact, even experienced researchers may miss subtle corner cases when designing RDTs for simple data structures. In this talk, I will discuss techniques for checking the correctness of RDTs and deriving correct-by-construction RDTs.
Carla Ferreira is an Associate Professor at Computer Science Department of the NOVA University of Lisbon, and a researcher at NOVA LINCS. Her research focuses on developing formal calculi, techniques, and tools to express and reason about concurrent and distributed systems with the ultimate goal of helping programmers build trustworthy and efficient systems. Currently, she leads the TaRDIS project, a Horizon Europe project centered around the correct and efficient development of applications for swarms and decentralized distributed systems.
In this talk I will discuss recent work on investigating the increase in observational capabilities of monitors that analyse systems over multiple runs. I will illustrate how this augmented monitoring setup can affect the class of properties that can be verified at runtime focussing, in particular, on branching-time properties expressed in the modal mu-calculus. Although branching-time properties are considered to be the preserve of static verification techniques such as model-checking, our preliminary results show that the extended monitoring setup can be used to systematically extend previously established monitorability limits. If time permits, I will also discuss bounds that capture the correspondence between the syntactic structure of a branching-time property and the number of system runs required to conduct adequate runtime verification.
This is joint work with Antonis Achilleos and Jasmine Xuereb.
Adrian Francalanza is a full professor at the University of Malta. His area of expertise covers both static and runtime verification, applied to behavioural models and languages for concurrency and distributed computation. He currently leads BehAPI: Behavioural APIs, an H2020 RISE project on behavioural theories for API-based software, and participates on a RANNIS project called MoVeMnt which aims to extend the theory and capabilities of runtime verification.