Gobra: Modular Specification and Verification of Go Programs (extended version)

TL;DR

Gobra is a modular verifier for Go that uses separation logic and SMT solving to ensure memory safety, crash safety, data-race freedom, and supports a large subset of the language.

Contribution

It introduces Gobra, a novel modular verification tool for Go that handles concurrency and mutable state using separation logic and translation to Viper.

Findings

Successfully verifies memory safety and data-race freedom in Go programs.

Supports a large subset of Go with automated proof obligations.

Uses existing SMT solvers for efficient verification.

Abstract

Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives. We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.