On the Monitorability of Session Types, in Theory and Practice (Artifact)

Authors Christian Bartolo Burlò , Adrian Francalanza , Alceste Scalas

Thumbnail PDF

Artifact Description

  • Filesize: 0.58 MB
  • 3 pages

Document Identifiers

Author Details

Christian Bartolo Burlò
  • Gran Sasso Science Institute, L'Aquila, Italy
Adrian Francalanza
  • Department of Computer Science, University of Malta, Msida, Malta
Alceste Scalas
  • DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark


This work has been partly supported by: the project MoVeMnt (No: 217987-051) under the Icelandic Research Fund; the BehAPI project funded by the EU H2020 RISE under the Marie Skłodowska-Curie action (No: 778233); the EU Horizon 2020 project 830929 CyberSec4Europe; the Danish Industriens Fonds Cyberprogram 2020-0489 Security-by-Design in Digital Denmark. The authors would like to thank the anonymous reviewers and Mario Alfonso Prado-Romero for testing the artifact and for providing useful feedback.

Cite AsGet BibTex

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)



In the paper "On the Monitorability of Session Types, in Theory and Practice" we study the monitorability of message-passing black-box processes against protocol specifications expressed as session types; we formalise a monitor synthesis procedure, prove its correctness, and discuss its implementation - as a tool that synthesises an executable monitor (in the Scala programming language) from a given session type. This artifact contains the aforementioned monitor synthesis tool, called STMonitor; it includes the tool source code, and documentation to reproduce the examples and benchmarks described in the paper.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Development frameworks and environments
  • Software and its engineering → Software verification and validation
  • Theory of computation → Concurrency
  • Session types
  • monitorability
  • monitor correctness
  • Scala


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Dummy. Google Scholar