Gobra: Modular Specification and Verification of Go Programs
OPEN ACCESS
Author / Producer
Date
2021
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Book title
Computer Aided Verification, 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I
Journal / series
Volume
12759
Pages / Article No.
367 - 379
Publisher
Springer
Event
33rd International Conference on Computer-Aided Verification (CAV 2021)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Separation logic; Program logics; Channel-based concurrency; Interfaces; Deductive verification; Automated verification
Organisational unit
03653 - Müller, Peter / Müller, Peter
Notes
Conference lecture held on July 20, 2021
Funding
87152 - NGI Pointer (EC)