4 citations · 14 across the 8 of their papers we have counts for
10 papers
Global Protocols under Rendezvous Synchrony: From Realizability to Type Checking
Elaine Li, Felix Stutz
Global protocol specifications are the starting point of top-down verification methodologies, and serve as a blueprint for synthesizing local specifications that guarantee the corr…
An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
Felix Stutz, Emanuele D'Osualdo
We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specif…
Characterizing Implementability of Global Protocols with Infinite States and Data
Elaine Li, Felix Stutz, Thomas Wies +1
We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. Our symbolic protocols describe infinite states a…
Deciding Subtyping for Asynchronous Multiparty Sessions
Elaine Li, Felix Stutz, Thomas Wies
Multiparty session types (MSTs) are a type-based approach to verifying communication protocols, represented as global types in the framework. We present a precise subtyping relatio…
Complete Multiparty Session Type Projection with Automata
Elaine Li, Felix Stutz, Thomas Wies +1
Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols rep…
Asynchronous Multiparty Session Type Implementability is Decidable -- Lessons Learned from Message Sequence Charts
Felix Stutz
Multiparty session types (MSTs) provide efficient means to specify and verify asynchronous message-passing systems. For a global type, which specifies all interactions between role…
Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types
Felix Stutz, Damien Zufferey
Communicating state machines provide a formal foundation for distributed computation. Unfortunately, they are Turing-complete and, thus, challenging to analyse. In this paper, we c…
Comparing Channel Restrictions of Communicating State Machines, High-level Message Sequence Charts, and Multiparty Session Types
Felix Stutz, Damien Zufferey
Communicating state machines provide a formal foundation for distributed computation. Unfortunately, they are Turing-complete and, thus, challenging to analyse. In this paper, we c…
Generalising Projection in Asynchronous Multiparty Session Types
Rupak Majumdar, Madhavan Mukund, Felix Stutz +1
Multiparty session types (MSTs) provide an efficient methodology for specifying and verifying message passing software systems. In the theory of MSTs, a global type specifies the i…
Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
Emanuele D'Osualdo, Felix Stutz
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographi…