Gobra: Modular specification and verification of Go programs
The work
| Authors | Felix A. Wolf; Linard Arquint; Martin Clochard; Wytse Oortwijn; João C. Pereira; Peter Müller |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2021 |
| Citekey | wolf2021gobra |
Where it appeared
| Published in | 33rd International Conference on Computer Aided Verification (CAV) |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 12759 |
| Volume | 12759 |
| Pages | 367--379 |
Identifiers
| DOI | 10.1007/978-3-030-81685-8_17 |
|---|
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.
A copy is held
pdf, 293.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-16 15:47 UTC |
Filed under
Cite it as
@inproceedings{wolf2021gobra,
title = {Gobra: Modular specification and verification of Go programs},
author = {Felix A. Wolf and Linard Arquint and Martin Clochard and Wytse Oortwijn and João C. Pereira and Peter Müller},
year = {2021},
booktitle = {33rd International Conference on Computer Aided Verification (CAV)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {12759},
pages = {367--379},
doi = {10.1007/978-3-030-81685-8_17},
}
This record lives at https://refs.drheap.org/wolf2021gobra/ and will keep doing so.