π-calculus, Session Types research at Imperial College

Session Type-Based Verification Framework for Message-Passing in Go
April 2017 - March 2021

This grant funded by VeTSS aims to research automated software verification and repair for programs written in Go with message passing through the use of channels.

This grant is associated to the PhD studentship of Julia, who works on using behavioural types and session types to model Go programs using channels. This work aims for the development of theory and tools to automate verification of properties on message-passing programs in Go, including checking for different kinds of errors through safety properties, ensuring channel liveness, and other extensions including data-race freedom in standard shared memory settings.
Related publications
Related tools
Go model checker for MiGo types, version 2

Godel2 is a model checker for MiGo types that returns results of liveness and safety checks for channels and mutex locks, as well as the presence of data races on shared pointers.