Published: 12th September 2019|
|Preface Massimo Bartoletti, Ludovic Henrio, Anastasia Mavridou and Alceste Scalas|
|Invited Presentation: Program Models for Compositional Verification Dilian Gurov|
|Invited Presentation: Smart Digital Contracts Fritz Henglein|
|Invited Presentation: Toward a Formal Model of Social Networks and Polarization Sophia Knight|
|Invited Presentation: Petri nets, Probabilities and Bayesian reasoning Hernán Melgratti|
|Interface Automata for Choreographies Hao Zeng, Alexander Kurz and Emilio Tuosto||1|
|Tracking Down the Bad Guys: Reset and Set Make Feasibility for Flip-Flop Net Derivatives NP-complete Ronny Tredup||20|
|A Note On Compliance Relations And Fixed Points. Maurizio Murgia||38|
|Rusty Variation: Deadlock-free Sessions with Failure in Rust Wen Kokke||48|
|Towards Gradually Typed Capabilities in the Pi-Calculus Matteo Cimini||61|
|Open Multiparty Sessions Franco Barbanera and Mariangiola Dezani-Ciancaglini||77|
|Detecting Architectural Erosion using Runtime Verification Diego Marmsoler and Ana Petrovska||97|
|The Cpi-calculus: a Model for Confidential Name Passing Ivan Prokić||115|
|On Learning Nominal Automata with Binders Yi Xiao and Emilio Tuosto||137|
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:
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.
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.
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.
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.