Project Description

This project will focus on designing techniques for specifying and checking properties of Go programs. Go [1] is a compiled, statically typed language developed at Google that is increasingly being used for high-performance computing applications, such as high-energy physics [9]. While experts have long successfully used formal languages such as Alloy [3] and VDM-SL [4] to specify & verify software properties, it is still difficult to write specifications in formal languages like these. An important goal will be to develop techniques for lightweight specification of Go programs inspired by semi-formal description languages like the ANSI C Specification Language (ACSL) [2]. This needs special attention to verifying concurrent software, the specification of which remains daunting despite decades of research. The project will involve exploiting the power of off-the-shelf constraint solvers like Z3 [5], and using verification tools such as Boogie [6], SMACK [7], and the Why3 system [8], to build a small prototype tool that can help automatically verify code written in Go.

References

[1] https://golang.org/

[2] https://frama-c.com/acsl.html

[3] http://alloytools.org/

[4] http://overturetool.org/

[5] https://github.com/Z3Prover/z3

[6] https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/

[7] https://smackers.github.io/

[8] http://why3.lri.fr/

[9] https://github.com/go-hep

Qualifications

1. A background in programming is needed;

2. Knowledge of C/C++ and some exposure to assembly language will be helpful;

3. Familiarity with a Unix-family/GNU Linux operating system and the free/open source software (FLOSS) ecosystem is a plus.