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.
@article{arxiv.2105.13840,
title = {Gobra: Modular Specification and Verification of Go Programs (extended version)},
author = {Felix A. Wolf and Linard Arquint and Martin Clochard and Wytse Oortwijn and João C. Pereira and Peter Müller},
journal= {arXiv preprint arXiv:2105.13840},
year = {2021}
}