Go Program Analysis and Verification

We are building a program analysis environment for the Go programming language using both Rascal and Maude.

Potential Projects

I am looking to work with students on the following projects related to this.

Concurrency Feature Usage in Go

What concurrency features do people actually use in Go? Do they just use message passing? Do they also use more traditional concurrency features like locks? Do these two styles of concurrency occur in separate parts of programs, or are they mixed together? This project will answer these questions by analyzing existing Go programs hosted on GitHub.

Formalizing the Go Language

Rewriting logic is a logic of concurrency which has been used to provide formal definitions of programming languages with concurrency support. We are currently creating a formal definition of Go using the Maude system which can then be used for program analysis and program verification, in tandem with an existing Go Analysis tool written in Rascal.

Models of IoT Systems

We are also looking at low code models for IoT. This is somewhat related to Go, since we are also looking at integrating Go into this, but we are actually interested more generally in techniques for understanding IoT systems and presenting useful information about these systems to developers.