Tools and software developed by our group.
Armus is a dynamic verification tool for deadlock detection and avoidance specialised in barrier synchronisation. Barriers are used to coordinate the execution of groups of tasks, and serve as a building block of parallel computing. Our tool verifies more barrier synchronisation patterns than current state-of-the-art. To improve the scalability of verification, we introduce a novel event-based representation of concurrency constraints, and a graph-based technique for deadlock analysis. The implementation is distributed and fault-tolerant, and can verify X10 and Java programs.
dingo-hunter is a static deadlock detection tool for the Go language.
The tool leverages session graph synthesis to detect potential deadlocks
and unsafe concurrency patterns in the source code.
effect-sessions library is an implementation of session types in
Haskell, via an effect system encoding by embedding session types into
an effect system.
The tool allows to
Gong is a liveness and safety checker for MiGo types.
HAPI is a programming language developed by Lasse Nielsen which provides an intuitive syntax for the asynchronous pi-calculus with multiparty session types.
lchannels is a Scala library for type-safe session programming. It provides linear I/O channels, which allow to transfer data locally, or over a network. Its API allows to
The Scala type checker can examine the resulting code and spot many protocol violations at compile time.
Pabble is a parametric extension of Scribble primarily designed for describing communication protocols in parallel computing.
The Scribble project is a joint effort with Cognizant, OOI and Red Hat established to realise multiparty session types as application-level protocols. It consists of a core language Scribble and tools/IDE support. A research version of Scribble is available from Raymond Hu, please contact him for details.
Session Actor is an actor framework in Python with support for session types. An actor can implement multiple session types (roles) in a similar way as an object can implement multiple interfaces. The framework supports automatic discovery of roles and runtime checks for protocol compliance.
Session C is a communication-safe programming framework which combines multiparty session types with the C programming language.
A Java extension with support for Session Types.
Session-ocaml is an implementation of session types in OCaml.
STP is a type provider in F# that generates APIs from protocol specifications.
This is an Erlang API for programming with gen_server.
We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. A recovered communication system is free from deadlocks, orphan messages and reception errors.