Skip to content. | Skip to navigation

Behavioural Types for Reliable Large-Scale Software Systems
COST Action IC1201

Navigation

You are here: Home / Tools

Tools

Members of BETTY have produced a number of software tools based on the theory of behavioural types.

  • SePi is an implementation of pi calculus with session types, developed at the University of Lisbon.
  • ProPi analyses message-passing systems for deadlocks, and verifies progress properties with respect to session types. It was developed at the University of Lisbon.
  • Hypha is a deadlock analysis tool for pi calculus, developed at the University of Torino.
  • Scribble is a language and tool set for defining and programming with communication protocols. It is being developed in a collaboration between Imperial College London, Red Hat, Cognizant and the Ocean Observatories Initiative.
  • Chor is a language for choreographic programming, developed at the University of Southern Denmark.
  • Links is a language for web programming, developed at the University of Edinburgh, which has an extension to include session types.
  • SJ (Session Java) is an extension of Java with session types, developed at Imperial College London.
  • The CO2 model checker is a tool for verifying honesty in contract-oriented systems. It was developed at the University of Cagliari.
  • The University of Cagliari has also developed a message-oriented middleware based on the theory of timed session types. It monitors communication between distributed components, guaranteeing safe interaction.
  • AIOCJ is a choreography programming language for adaptable systems, which guarantees deadlock-freedom in a way that is preserved during adaptation. It was developed at the University of Bologna.
  • ChoSyn implements a correspondence between communicating finite state machines and graphical choreographies. It was developed at the University of Leicester and Imperial College London. There are two versions: a prototype and a more recent version.
  • HAPI is a language for protocol verification, based on typed pi-calculus. It was developed at the University of Copenhagen.
  • Mungo is a typestate checker for Java, which enforces constraints on the order in which methods can be called. StMungo translates Scribble local protocols into Mungo typestate specifications, enabling protocol roles to be implemented and statically typechecked in Java. Both tools were developed at the University of Glasgow.
  • ParTypes is a toolchain for validating and synthesising message-based programs for Message Passing Interface (MPI) programs. It was developed at the University of Lisbon.
  • effect-sessions is an implementation of session types in Haskell, based on an embedding of session types into an effect system. It was developed at Imperial College London.
  • DinGo Hunter is a static deadlock detection tool for the Go programming language, based on synthesis of session graphs. It was developed at Imperial College London.
  • AdaptEr is an runtime adaptation monitoring tool for Erlang. It was developed at the University of Malta.
  • FuSe is an OCaml module for session types. It was developed at the University of Torino. 
  • Deaf Parrot is a type checker for rely-guarantee protocols on shared mutable state. It was developed at NOVA University of Lisbon and Carnegie Mellon University.
  • DF4ABS is a deadlock and livelock analyser for ABS (Abstract Behavioural Specification Language). It was developed at the University of Bologna.
  • SRA is a static resource analyser for a concurrent object-oriented language. It was developed at the University of Bologna.
  • IT University of Copenhagen has developed a set of tools for business process modelling, based on DCR Graphs.