Preface

This volume contains the proceedings of ICE'19, the 12th Interaction and Concurrency Experience, which was held in Copenhagen, Denmark on the 20th and 21st of June 2019, as a satellite event of DisCoTec'19. 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), and DisCoTec'18 (Madrid, Spain).

The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged 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 editions, the forum discussion during the review and selection phase of ICE'19 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.

The 2019 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. Each paper was reviewed by three PC members, and altogether 9 papers were accepted for publication - plus 2 oral presentations which are not part of this volume. We were proud to host 4 invited talks, by Dilian Gurov, Fritz Henglein, Sophia Knight, and Hernán Melgratti. 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 Dilian Gurov, Fritz Henglein, Sophia Knight, and Hernán Melgratti for accepting our invitations to present their recent work. We are grateful for the efforts of the PC members:

• Aimée Borda (Trinity College Dublin, IE)
• Matteo Cimini (University of Massachusetts Lowell, USA)
• Corina Cirstea (University of Southampton, UK)
• Ornela Dardha (University of Glasgow, UK)
• Simon Fowler (University of Edinburgh, UK)
• Svetlana Jakši ć (Western Norway University of Applied Sciences, NO)
• Sophia Knight (University of Minnesota Duluth, USA)
• Ivan Lanese (University of Bologna, IT)
• Julien Lange (University of Kent, UK)
• Hugo-Andrés López (IT University of Copenhagen and DCR Solutions, DK)
• Hernán Melgratti (University of Buenos Aires, AR)
• Claudio Antares Mezzina (University of Leicester, UK)
• Maurizio Murgia (University of Cagliari, IT)
• Kristin Peters (TU Berlin, DE)
• Matteo Sammartino (University College London, UK)
• Emmanouela Stachtiari (Aristotle University of Thessaloniki, GR)
• Silvia Lizeth Tapia Tarifa (University of Oslo, NO)
• Hugo Torres Vieira (IMT Lucca, IT)
• Johannes Åman Pohjola (Data61/CSIRO, AU)

Program Models for Compositional Verification

Dilian Gurov (KTH, Sweden)

Verification of procedural programs typically faces the problem of scalability. To tackle this problem, most tools for deductive verification are procedure-modular: every procedure is verified separately, in isolation, relying on the contracts of the procedures it calls. For temporal properties, however, modularity poses certain difficulties. In this talk we will show how procedure modularity can be achieved by using a program model called flow graphs. Flow graphs can be extracted from program code, but can also be constructed from logical specifications. In a first instalment of the framework, flow graphs will only model the control flow of programs. Extending the framework to also represent program data will lead us to use the concept of action, which in this context refers to a state change specified in logic. We will see that a similar approach allows us to also deal with concurrent programs, where actions model exclusive accesses to shared memory.

Smart Digital Contracts

Fritz Henglein (University of Copenhagen and Deon Digital, Denmark)

The term ‘smart contract’ was informally introduced as “a computerized transaction protocol that executes the terms of a contract” (Szabo, 1994). It has been popularized in Ethereum, where it is an object encapsulating an account balance, written in a reactive, object-oriented programming language that is executed on a decentralized replicated deterministic state machine (Buterin, 2014; Wood, 2014). Based on the REA accounting model (McCarthy, 1982) and a semantic model of contracts as event sequence classifiers (Andersen et al, 2006), we deconstruct a smart contract into a digital contract with a formal mathematical semantics that represents the terms of a contract; its life-cycle management, which executes, validates and monitors contract events; and its resource management (who owns what) in both decentralized (blockchain/distributed ledger) and centralized systems. We describe CSL, a compositional digital contract specification language in use and active development at Deon Digital (https://hub.docker.com/r/deondigital/vitznauerstock) and report on formalizing its denotational and operational semantics and proving their coherence in Coq as a basis for guaranteed sound static analysis and certified security guarantees.

Toward a Formal Model of Social Networks and Polarization

Sophia Knight (University of Minnesota Duluth, USA)

We will present a preliminary model for social networks, and a measure of the level of polarization in these social networks, based on Esteban and Ray 's classic measure of polarization for economic situations. The models include information about each agent's quantitative strength of belief in a proposition of interest and a representation of the strength of each agent's influence on every other agent. We consider how the model changes over time as agents interact and communicate, and include several different options for belief update, including rational belief update and update taking into account irrational responses such as confirmation bias and the backfire effect. Under various scenarios, we consider the evolution of polarization over time, and the implications of these results for real world social networks. I will discuss several directions for future work, including new polarization measures, probabilistic update, and an epistemic logic suited for this model of social networks.

Petri nets, Probabilities and Bayesian reasoning

Hernán Melgratti (University of Buenos Aires - Conicet, Argentina)

In this talk we will explore the connections between Petri nets (PN) and Bayesian networks (BN). Despite these two models have different purpose, they share a similar structure, which becomes evident when equipping PN with a suitable probabilistic structure. We will show that this connection provides different views for the same model: the standard token game of the PN view gives a concrete, probabilistic computational model; while BN semantics allows us to reason about properties of the underlying concrete model.