Description: Concurrent typestate-oriented programming for Java Developed at: UNITO Contacts: Luca Padovani Available at: http://www.di.unito.it/~padovani/Software/EasyJoin/

Description: It synthesises Erlang monitors from mu-HML specifications and instruments them with the system under scrutiny Developed at: UOM Contacts: duncan.attard.01@um.edu.mt, ian.cassar.10@um.edu.mt, afra1@um.edu.mt Available at: https://bitbucket.org/duncanatt/detecter-lite https://bitbucket.org/casian/adapter https://bitbucket.org/casian/detecter2.0

Description: Industrial tool supporting a graphs process notation developed for the formalisation and mechanisation of adaptive case management processes. DCR (Dynamic Condition Response) graphs features (a) a (declarative) process language

Description: The tool introduces a domain-specific language for OpenAPI specifications, COpenAPI, that enables the modelling of communication protocols between a REST client and server. From these COpenAPI specifications, the tool generates

Description: Academic prototype to build enabledness-based program abstractions (EPAs) out of APIs written in C and pre/post contracts written in (a kind of) FOL. Contractor generates a finite abstraction representing

Description: Corinne is a tool working on choreography automata (FSA where transitions are labelled by interactions A -> B:m), performing visualization, product, synchronization and projection. Developed at: UNIBO Contacts: ivan.lanese@gmail.com Available

Description: Automatic test generator based on G-choreographies. It is well documented tool papers and the PhD thesis of Alex Coto (to appear) Developed at: GSSI Contacts: Emilio Tuosto Available at: https://bitbucket.org/eMgssi/chorgram/

Description: The main functionalities offered by CobaltBlue are the checking of protocol conformance and deadlock analysis of concurrent objects implemented with typestate-oriented programming. The tool is based on behavioral type checking