Title
Gobra: Modular Specificationand Verification of Go Programs
Author
Wolf, F.A.
Arquint, L.
Clochard, M.
Oortwijn, W.
Pereira, J.C.
Müller, P.
Contributor
Silva, A. (editor)
Leino, K.R.M. (editor)
Publication year
2021
Abstract
Go is an increasingly-popular systems programming lan-guage targeting, especially, concurrent and distributed systems. Go dif-ferentiates itself from other imperative languages by offering structuralsubtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interestingchallenges for static verification, most prominently the combination of amutable heap and advanced concurrency primitives.We present Gobra, a modular, deductive program verifier for Gothat proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supportsa large subset of Go. Its implementation translates an annotated Goprogram into the Viper intermediate verification language and uses anexisting SMT-based verification backend to compute and discharge proofobligations.
Subject
Separation logic
Program logics
Channel-basedconcurrency
Interfaces
Deductive verification
Automated verification
Industrial Innovation
To reference this document use:
http://resolver.tudelft.nl/uuid:2c2334c4-e126-4ff3-b34a-61897c36de27
DOI
https://doi.org/10.1007/978-3-030-81685-8_17
TNO identifier
957880
Publisher
Springer Verlag, Cham
ISBN
9783030816858
ISSN
0302-9743
Source
Lecture Notes in Computer Science, 12759 (12759), 367-379
Series
Lecture Notes in Computer Science
Bibliographical note
33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021
Document type
conference paper