ICE 2023 - 16th Interaction and Concurrency Experience

Interaction and Concurrency Experiences (ICE) is a series of international scientific meetings oriented to theoretical computer science researchers with special interest in models, verification, tools, and programming primitives for concurrent systems and complex interactions. ICE 2023 is a satellite workshop of DisCoTec 2023, held on Monday 19th June 2023 at the NOVA University in Lisbon, Portugal.

Highlights

Scope

The general scope of the venue includes theoretical and applied aspects of interactions and the synchronization mechanisms used among components of concurrent/distributed systems, related to several areas of computer science in the broad spectrum ranging from formal specification and analysis to studies inspired by emerging computational models.

We solicit contributions relevant to Interaction and Concurrency, including but not limited to:

Accepted Papers

Programme and Pre-proceedings

You can download the ICE 2023 pre-proceedings, and the slides or presentation below by clicking on the talk title.

The proceedings are also available as EPTCS 383.

The talks will take place at Room 219 at Colégio Almada Negreiros.

All times are listed for WEST (Western European Summer Time)

Time WEST Session Talk
9:00-9:10 Opening Welcome to ICE 2023
9:10-10:10 Invited talk Carla Ferreira
10:10-10:40 Co-ordination (Chair: Simon Fowler) Type qualifier inference and code synthesis for a better data-centric synchronisation experience (Oral Communication) (Ana Almeida Matos, António Ravara, Hervé Paulino, Jan Cederquist, João Matos and Marco Giunti)
10:40-11:10   Research Challenges in Orchestration Synthesis (Davide Basile and Maurice H ter Beek)
11:10-11:30 Coffee break  
11:30-12:00 Semantics (Chair: Davide Basile) Branching pomsets and event structures (Oral Communication) (Luc Edixhoven, Sung-Shik Jongmans, José Proença and Ilaria Castellani)
12:00-12:30   Algebraic Reasoning About Timeliness (Seyed Hossein Haeri, Peter Van Roy, Peter Thompson, Magne Haveraaen, Neil Davies, Mikhail Barash, Kevin Hammond and James Chapman)
12:30-13:00   On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues (Manel Barkallah and Jean-Marie Jacquet)
13:00-14:30 Lunch break  
14:30-15:30 Invited talk Adrian Francalanza
15:30-16:00 Runtime Verification (Chair: Simon Fowler) Revisiting Benchmarking for Concurrent Runtime Verification (Oral Communication) (Duncan Paul Attard)
16:00-16:30 Coffee break  
16:30-17:00 Confidentiality & Communication (Chair: Duncan Paul Attard) Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing (Oral Communication) (Muhammad Usama Sardar, Thomas Fossati and Simon Frost)
17:00-17:30   Partially Typed Multiparty Sessions (Franco Barbanera and Mariangiola Dezani-Ciancaglini)
17:30-18:00   Proofs about Network Communication: For Humans and Machines (Wolfgang Jeltsch and Javier Díaz)
19.00-20.00 Welcome reception  

Invited Speakers

Carla Ferreira

Talk: Techniques for safe and highly available cloud applications

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.

Biography

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.

Adrian Francalanza

Talk: If At First You Don’t Succeed: Extended Monitorability through Multiple Executions

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 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.

Biography

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.

Important Dates

The following dates are in the Anywhere on Earth time zone.

The ICE Selection Procedure

Since its first edition in 2008, the distinguishing feature of ICE has been an innovative paper selection mechanism based on an interactive, friendly, and constructive discussion amongst authors and PC members in an online forum.

During the review phase, each submission is published in a dedicated discussion forum. The discussion forum can be accessed by the authors of the submission and by all PC members not in conflict with the submission (the forum preserves anonymity). The forum is used by reviewers to ask questions, clarifications, and modifications from the authors, allowing them better to explain and to improve all aspects of their submission. The evaluation of the submission will take into account not only the reviews, but also the outcome of the discussion.

As witnessed by the past editions of ICE, this procedure considerably improves the accuracy of the reviews, the fairness of the selection, the quality of camera-ready papers, and the discussion during the workshop.

ICE adopts a light double-blind reviewing process, detailed below.

Submission Guidelines

Submissions must be made electronically in PDF format via OpenReview.

We invite two types of submissions:

Authors of research papers must omit their names and institutions from the title page, they should refer to their other work in the third person and omit acknowledgements that could reveal their identity or affiliation. The purpose is to avoid any bias based on authors’ identity characteristics, such as gender, seniority, or nationality, in the review process. Our goal is to facilitate an unbiased approach to reviewing by supporting reviewers’ access to works that do not carry obvious references to the authors’ identities. As mentioned above, this is a lightweight double-blind process. Anonymization should not be a heavy burden for authors, and should not make papers weaker or more difficult to review. Advertising the paper on alternate forums (e.g., on a personal web-page, pre-print archive, email, talks, discussions with colleagues) is permitted, and authors will not be penalized by for such advertisement.

Papers in the “Oral communications” category need not be anonymized. For any questions concerning the double blind process, feel free to consult the ICEcreamers.

We are keen to enhance the balanced, inclusive and diverse nature of the ICE community, and would particularly encourage female colleagues and members of other underrepresented groups to submit their work.

Publications

Accepted research papers and communications must be presented at the workshop by one of the authors.

Accepted research papers will be published after the workshop in Electronic Proceedings in Theoretical Computer Science.

We plan to invite authors of selected papers and brief announcements to submit their work in a special issue in the Journal of Logical and Algebraic Methods in Programming (Elsevier) (to be confirmed). Such contributions will be regularly peer-reviewed according to the standard journal policy, but they will be handled in a shorter time than regular submissions. A list of published and in preparation special issues of previous ICE editions is reported below.

ICEcreamers

Use ice (at) framalistes.org to reach all the ICEcreamers at once.

Programme Committee

★ The ICE 2023 Outstanding PC Member Award was awarded to Sergueï Lenglet!

Steering Committee

Previous Editions

The previous editions of ICE have been held on:

More Information

For additional information, please contact the ICEcreamers at ice (at) framalistes.org.

Sponsors

ICE acknowledges the generous support of EAPLS through its support for workshops initiative.

European Association for Programming Languages and Systems