35 citations · 63 across the 23 of their papers we have counts for
24 papers
NEST: Network Enforced Session Types (Technical Report)
Jens Kanstrup Larsen, Alceste Scalas, Guy Amir +3
This paper introduces NEST (Network-Enforced Session Types), a runtime verification framework that moves application-level protocol monitoring into the network fabric. Unlike prior…
Compositional Design, Implementation, and Verification of Swarms (Technical Report)
Florian Furbach, Lucas Clorius, Roland Kuhn +3
Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called ma…
JoinActors: A Modular Library for Actors with Join Patterns
Ayman Hussein, Philipp Haller, Ioannis Karras +3
Join patterns are a high-level programming construct for message-passing applications. They offer an intuitive and declarative approach for specifying how concurrent and distribute…
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
Radosław Jan Rowicki, Adrian Francalanza, Alceste Scalas
Many software applications rely on concurrent and distributed (micro)services that interact via message-passing and various forms of remote procedure calls (RPC). As these systems…
On Asynchronous Multiparty Session Types for Federated Learning
Ivan Prokić, Simona Prokić, Silvia Ghilezan +2
This paper improves the session typing theory to support the modelling and verification of processes that implement federated learning protocols. To this end, we build upon the asy…
Encoding Petri Nets into CCS (Technical Report)
Benjamin Bogø, Andrea Burattin, Alceste Scalas
This paper explores the problem of determining which classes of Petri nets can be encoded into behaviourally-equivalent CCS processes. Most of the existing related literature focus…
Behavioural Types for Heterogeneous Systems (Position Paper)
Simon Fowler, Philipp Haller, Roland Kuhn +3
Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of b…
COTS: Connected OpenAPI Test Synthesis for RESTful Applications
Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas +1
We present a novel model-driven approach for testing RESTful applications. We introduce a (i) domain-specific language for OpenAPI specifications and (ii) a tool to support our met…
P4R-Type: a Verified API for P4 Control Plane Programs (Technical Report)
Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller +1
Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The de facto standard for progr…
Proceedings 14th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software
Ilaria Castellani, Alceste Scalas
This volume contains the proceedings of PLACES 2023, the 14th edition of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The PLAC…
PSTMonitor: Monitor Synthesis from Probabilistic Session Types
Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas +2
We present PSTMonitor, a tool for the run-time verification of quantitative specifications of message-passing applications, based on probabilistic session types. The key element of…
Proceedings 15th Interaction and Concurrency Experience
Clément Aubert, Cinzia Di Giusto, Larisa Safina +1
This volume contains the proceedings of ICE'22, the 15th Interaction and Concurrency Experience, which was held as an hybrid event in Lucca, Italy, and as a satellite event of DisC…
Generalised Multiparty Session Types with Crash-Stop Failures (Technical Report)
Adam D. Barwell, Alceste Scalas, Nobuko Yoshida +1
Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we pres…
Proceedings 14th Interaction and Concurrency Experience
Julien Lange, Anastasia Mavridou, Larisa Safina +1
This volume contains the proceedings of ICE'21, the 14th Interaction and Concurrency Experience, which was held online on the 18th of June 2021, as a satellite event of DisCoTec'21…
Towards Probabilistic Session-Type Monitoring
Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas +2
We present a tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types. We synthesise a monitor out of a probabilistic…
Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić +2
This paper presents the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees s…
Proceedings 13th Interaction and Concurrency Experience
Julien Lange, Anastasia Mavridou, Larisa Safina +1
This volume contains the proceedings of ICE'20, the 13th Interaction and Concurrency Experience, which was held online on the 19th of June 2020, as a satellite event of DisCoTec'20…
A formal model of Algorand smart contracts
Massimo Bartoletti, Andrea Bracciali, Cristian Lepore +2
We develop a formal model of Algorand stateless smart contracts (stateless ASC1.) We exploit our model to prove fundamental properties of the Algorand blockchain, and to establish…
Proceedings 12th Interaction and Concurrency Experience
Massimo Bartoletti, Ludovic Henrio, Anastasia Mavridou +1
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 satel…
Multiparty Session Types, Beyond Duality (Abstract)
Alceste Scalas, Nobuko Yoshida
Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing ca…
On the Preciseness of Subtyping in Session Types
Tzu-chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas +1
Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usuall…
The LTS WorkBench
Alceste Scalas, Massimo Bartoletti
Labelled Transition Systems (LTSs) are a fundamental semantic model in many areas of informatics, especially concurrency theory. Yet, reasoning on LTSs and relations between their…
Choreography Synthesis as Contract Agreement
Julien Lange, Alceste Scalas
We propose a formal model for distributed systems, where each participant advertises its requirements and obligations as behavioural contracts, and where multiparty sessions are st…
Honesty by Typing
Massimo Bartoletti, Alceste Scalas, Emilio Tuosto +1
We propose a type system for a calculus of contracting processes. Processes can establish sessions by stipulating contracts, and then can interact either by keeping the promises ma…