Published: 4th October 2018|
|Preface Massimo Bartoletti, Sophia Knight, Laura Bocchi and Ludovic Henrio|
|From the Parts to the Whole; Formal Methods in Action Silvia Crafa||1|
|Constrained DPOR: Avoiding Redundancies in the Exploration of Concurrent Programs Elvira Albert||2|
|Reasoning about Consistency Choices in Modern Distributed Systems Alexey Gotsman||3|
|Global Types for Open Systems Franco Barbanera, Ugo de'Liguoro and Rolf Hennicker||4|
|Toward a Uniform Approach to the Unfolding of Nets Eric Fabre and G. Michele Pinna||21|
|Realisability of Pomsets via Communicating Automata Roberto Guanciale Dr and Emilio Tuosto Dr||37|
|Prototyping Formal System Models with Active Objects Eduard Kamburjan and Reiner Hähnle||52|
|Unfolding of Finite Concurrent Automata Alexandre Mansard||68|
|On Urgency in Asynchronous Timed Session Types Maurizio Murgia||85|
This volume contains the proceedings of ICE'18, the 11th Interaction and Concurrency Experience, which was held in Madrid, Spain on the 20th and 21st of June 2018 as a satellite event of DisCoTec'18. 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), and Discotec'17 (Neuchâtel, Switzerland).
The ICE workshop series features a distinguishing review and selection procedure, allowing PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions that the authors reply to. As in the past ten editions, the forum discussion during the review and selection phase of ICE'18 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 forum interaction is rewarding for both authors, in revising their papers, and reviewers, in writing their reviews: the forum discussion makes 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.
For the second time, the 2018 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Papers were blinded for submission, with authors' names and identifying details removed, and authors were given anonymous usernames for the forum. When the review process was finished, in a survey, reviewers mostly expressed satisfaction with double blind reviewing and support for its future use.
Each paper was reviewed by three PC members, and altogether six papers were accepted for publication (the workshop also featured four oral presentations which are not part of this volume). We were proud to host three invited talks, by Elvira Albert, Silvia Crafa, and Alexey Gotsman. The abstracts of these talks are included in this volume together with the regular papers. Final versions of the contributions, taking into account the discussion at the workshop, are included.
We would like to thank the authors of all the submitted papers for their interest in the workshop. We thank Elvira Albert, Silvia Crafa, and Alexey Gotsman for accepting our invitations to present their recent work. We are grateful for the efforts of the PC members:
We thank the ICE steering committee and the DisCoTec'18 organizers, in particular the general and workshop chairs, for providing an excellent environment for the preparation and staging of the event. Finally, we thank the editors of EPTCS for the publication of this post-proceedings.
I will present a couple of research projects showing how Concurrency -and Interaction, which is its key ingredient- is addressed at different abstraction levels, ranging from the epistemic level to the programming primitives. We will see concurrency theory in action in modelling a financial system, in choosing a framework for programming the behaviour of interactive entities, and in formally reasoning about a system of concurrent objects.
Verification and testing of concurrent programs is challenged by the combinatorial explosion that arises by considering all possible ways in which processes/threads can interleave. Partial Order Reduction (POR) techniques avoid redundancies in the exploration of concurrent programs based on the idea that two interleavings can be considered equivalent if one can be obtained from the other by swapping adjacent, independent execution steps. This talk will overview recent context-sensitive, constrained, dynamic POR techniques incorporated in the SYCO system, a SYstematic testing tool for COncurrent programs. We will also describe recent applications of SYCO to verify Software-Defined Networks.
Distributed systems underlying large-scale Internet services often guarantee immediate availability and tolerate network failures at the expense of providing only weak data consistency guarantees. This is compensated for by new programming constructs, such as replicated data types (aka CRDTs) and novel forms of transactions. Navigating the spectrum of possible consistency models and programming constructs is far from trivial. I will survey recent developments that help in this: formal definitions of consistency model semantics and methods for reasoning about how the weakness of consistency models affects the correctness of applications using them.