Recent or ongoing stuff
- MoCheQoS: Automated Analysis of Quality of Service Properties of Communicating Systemswith Carlos G. Lopez Pombo and Agustín E. Martinez Suñé.
A tool implementing the stuff published at ICTAC 2023
Submitted.
Available here
- A Dynamic Temporal Logic for Quality of Service in Choreographic Modelswith Carlos G. Lopez Pombo and Agustín E. Martinez Suñé.
Using choreographies to analyse QoS of communicating systems
ICTAC 2023 (in print).
Available here
- Behavioural Types for Local-First Softwarewith Hernán Melgratti and Roland Kuhn.
The title says it all.
ECOOP 2023 (an extended version is at https://doi.org/10.48550/arXiv.2305.04848).
Available here
- A Theory of Formal Choreographic Languageswith Ivan Lanese and Franco Barbanera.
The extended version of our Coordination 2022 paper
LMCS 19(3) 2023.
Available here
- Composition of Synchronous Communicating Systemswith Ivan Lanese and Franco Barbanera.
The extended version of our ICE 2022 paper
JLAMP 135:1000890 2023.
Available here
- Formal Choreographic Languageswith Ivan Lanese and Franco Barbanera.
A model of choreographies based on formal languages
Coordination 2022.
Available here
- PSTMonitor: Monitor synthesis from probabilistic sessionwith Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas, and Catia Trubiani.
PSTMonitor, a tool for the run-time verification of quantitative specifications of message-passing applications, based on probabilistic session types
SCICO 2022.
Available here
- Design-by-Contract for Flexible Multiparty Session Protocols (Artifact)with Lorenzo Gheri, Ivan Lanese, Neil Sayers, and Nobuko Yoshida.
A tool supporting web development via choreography automata
ECOOP 2022.
Available here
- Design-by-Contract for Flexible Multiparty Session Protocolswith Lorenzo Gheri, Ivan Lanese, Neil Sayers, and Nobuko Yoshida.
DbC using choreography automata
ECOOP 2022.
Available here
- A Prototype for Data Race Detection in CSeq 3 - (Competition Contribution).with Alex Coto, Omar Inverso, and Emerson Sales.
Chasing data races in C programs
TACAS 2022.
Available here
- On Composing Communicating Systemswith Franco Barbanera and Ivan Lanese.
An approach to composing communicating systems in the asymmetric synchronous case.
ICE 2022.
Available here
- An Abstract Framework for Choreographic Testingwith Alex Coto and Roberto Guanciale.
Model-driven testing based on choreographies…a first step. We introduce admissible tests and show how to derive them from global specifications.
JLAMP.
Available here
- Towards Probabilistic Session-Type Monitoringwith Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas, and Catia Trubiani.
A tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types.
COORDINATION 2021.
Available here
- PomCho: a tool chain for choreographic designwith Roberto Guanciale.
The paper describes a tool chain for model-driven development of asynchronous message-passing applications.
SCICO.
Available here
- On Resolving Non-determinism in Choreographieswith Laura Bocchi and Hernán Melgratti.
The paper introduces the idea of whole spectrum realisation and a type system to enforce this property.
LMCS.
Available here
- Towards Refinable Choreographieswith Ugo de’Liguoro and Hernán Melgratti.
We investigate refinement in the context of choreographies allowing for the underspecification of protocols through refinable interactions. A typing discipline enforces well-formedness. (The ICE version is here)
JLAMP 2020.
Available here
- Abstractions for Collective Adaptive Systemswith Omar Inverso and Catia Trubiani.
Mumbling about what behavioural types suit Collective Adaptive Systems.
ISoLA 2020.
Available here
- An Abstract Framework for Choreographic Testingwith Alex Coto and Roberto Guanciale.
Model-driven testing based on choreographies…a first step. We introduce admissible tests and show how to derive them from global specifications.
ICE 2020.
Available here
- On Testing Message-Passing Componentswith Alex Coto and Roberto Guanciale.
An instance of the abstract framework for testing with a non-trivial example.
ISoLA 2020.
Available here
- Composition and Decomposition of Multiparty Sessionswith Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ivan Lanese.
A compositional framework of open global types where two participants act as coupled gateways forwarding messages between the two sessions. We show that the session resulting from the composition can be typed starting from global types. Lock-freedom is preserved by composition. We also propose a decomposition operator which is the left inverse of direct composition.
JLAMP.
Available here
- Composing Communicating Systems, Synchronouslywith Franco Barbanera and Ivan Lanese.
As in the previous draft, but in a setting based on automata. We discuss how to ensure relevant communication (eg deadlock freedom) in a compositional way. The idea is that communicating systems can be composed by transforming two of their participants andthem into coupled forwarders. The synchronous case is surprisingly intriguing.
ISoLA 2020.
Available here
- Choreography Automatawith Franco Barbanera and Ivan Lanese.
We introduce choreography automata for the choreographic modelling of communicating systems, project them on communicating finite-state machines, and consider both the standard asynchronous semantics of communicating systems and a synchronous variant of it. For both, the projections of well-formed automata are proved to be live as well as lock- and deadlock-free.
COORDINATION 2020.
Available here
- A Choreography-Driven Approach to APIs: the OpenDXL Case Studywith Leonardo Frittelli, Facundo Maldonado, Hernán Melgratti, and Emilio Tuosto.
We propose a model-driven approach based on choreographies. The paper reports on the application of our approach to the threat intelligence exchange (TIE) services provided by McAfee through the OpenDXL industrial platform.
COORDINATION 2020.
Available here
- Choreographic Development of Message-Passing Applications - A Tutorialwith Alex Coto, Roberto Guanciale, Emilio Tuosto.
A tutorial on some recent ideas to harness choreographic development of message-passing software supported by the ChorGram toolchain.
COORDINATION 2020.
Available here
Contributed collections
- Message-passing, choreographically. Mathematical Foundations of Software Engineering. Essays in Honour of Tom Maibaum on the Occasion of his 70th Birthday and Retirement. Contribution co-authored with Hernán Melgratti and Ugo de’Liguoro Available Here
- Data-Driven Choreographies à la Klaim. Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday. Contribution co-authored with Roberto Bruni, Andrea Corradini, Fabio Gadducci, Hernán C. Melgratti, and Ugo Montanari Available Here
- Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods. Contribution co-authored with Giancarlo Bigi, Andrea Bracciali, and Giovanni Meacci Available Here
- Towards Choreographic-Based Monitoring. Selected Results of the COST Action IC1405. Contribution co-authored with Adrian Francalanza and Claudio Antares Mezzina Available Here
- Chapter 1: Contract-Oriented Design of Distributed Applications: A Tutorial and Chapter 6: A Tool for Choreography-Based Analysis of Message-Passing Software. One of the outputs of the BETTY Cost Action. Chapter 1 co-authored with Nicola Atzei, Massimo Bartoletti, Maurizio Murgia, and Roberto Zunino; Chapter 6 co-authored with Julien Lange and Nobuko Yoshida Available Here
- [1] A Formal Support to Business and [2] Architectural Design for Service-Oriented Systems and Model-Driven Development of Long Running Transactions. Results of the SENSORIA Project 2011. Contribution [1] co-authored with Roberto Bruni, Howard Foster, Alberto Lluch Lafuente, and Ugo Montanari; Contribution [2] co-authored with Vincenzo Ciancia, Gianluigi Ferrari, Roberto Guanciale, and Daniele Strollo Available Here
- A Formal Basis for Reasoning on Programmable QoS. Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. Contribution co-authored with Rocco De Nicola, Gianluigi Ferrari, Ugo Montanari, and Rosario Pugliese Available Here
Edited volumes
LMCS, November 2019
LNCS 11533, June 2019
Volume 9, Issue 3-4, September 2015
LNCS 8902, TGC 2014
EPTCS 12
ENTCS 229(3)
ECEASST 16