MobilityReadingGroup

Session Type-Based Verification Framework for Message-Passing in Go

April 2017 - March 2021

vetss-session

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.

https://vetss.org.uk/funded-proposals/

• Prof Nobuko Yoshida

  PI, Imperial College London