Supervisors

Suitable for

Abstract

Prerequisites:  Familiarity with model-checking and behavioural types is helpful, but not required

Background

The Go programming language has seen widespread adoption in industry due to its efficient blend of systems programming and concurrency. Its concurrency primitives, influenced by process calculi like CCS and CSP, utilise channel-based communication and lightweight threads, offering a unique approach to structuring concurrent software. Concurrency bugs, such as deadlocks and safety violations, are common in Go programs and can lead to crashes, unpredictable behaviour, or resource leaks. There have been efforts to verify concurrency in Go programs using behavioural types and model checking [1, 2, 3]. These approaches model dynamic communication patterns to analyse concurrent behaviour. While effective, challenges remain in handling complex language features, reducing false positives, and improving scalability for real-world applications.

Focus

This project aims to advance techniques for verifying the correctness of concurrent Go programs, building on existing research in behavioural types and model checking. The project will focus on addressing challenges in analysing Go’s dynamic concurrency structures, such as runtime-determined goroutines and channel usage.

Method

Key objectives include improving the precision and scalability of verification techniques, extending support for advanced Go concurrency features like recursive goroutine spawning, and developing automated methods for detecting and classifying bugs.

Essential goals: Extend verification techniques for advanced Go concurrency features such as barriers and recursive gorouting spawining.

Stretch goals: Develop methods for detecting and classifying bugs, and improve the over-approximation methods of program translation.