Developing IDE Support for a Golang Verifier
external page Go is a modern programming language with a focus on simple and scalable concurrency. It is used in large-scale web-based software projects, such as Netflix, Ethereum, and Scion.
As experienced in cases such as external page Heartbleed, bugs in these systems can have severe consequences, compromising confidential user data and costing large sums of money. Testing and similar techniques can increase confidence in the correctness of code. However, they do not provide strong guarantees about the absence of bugs.
Gobra is a deductive verification tool for Go programs, developed in our group. It allows developers to write contracts and annotations in the source code, which are then used to automatically check the functional correctness of the program. Internally, Gobra translates Go programs to the Viper intermediate verification language.
Currently, Gobra is run as a command-line tool and has no IDE integration. This limits productivity when working with the tool and makes it challenging to integrate Gobra verification into a larger project.
Goals
The aim of this project is to develop an IDE integration for Gobra that provides a smooth user experience for Go code verification. The core milestones of this project are:
● Implement a Gobra IDE plugin for Visual Studio Code. This involves implementing support for standard IDE features such as syntax highlighting and error reporting, as well as a Gobra server mode that allows verifying multiple files without restarting the Gobra process, which is crucial for interactive verification. An IDE for Viper already exists, which can be used as a baseline.
● Optimize Gobra to be responsive enough for daily development, by applying performance optimization techniques, such as caching, and by improving user experience, for example by enabling to switch from code verification to code development and vice versa.
Opportunities
● Obtain an understanding of deductive verification techniques and how they are used in practice.
● Contribute to a state-of-the-art deductive verifier that is at the center of a large ongoing research project.
● Gain experience with the development of programming assisting tools.
Prerequisites
Major parts of Gobra are implemented in Scala. Therefore, prior experience programming in Scala would be beneficial, but is not required.