Gobra: Modular Specificationand Verification of Go Programs
conference paper
Gobra 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 go routines 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 Go that 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.
Topics
TNO Identifier
957880
ISSN
03029743
ISBN
978-3-030-81685-8
Publisher
Springer Verlag
Source title
International Conference on Computer Aided Verification
Editor(s)
Silva, A.
Leino, K.R.M.
Leino, K.R.M.
Place of publication
Cham
Pages
367-379