Gobra
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
Go is targeted at high performance applications running in potentially distributed settings and on multicore machines. Hence, Go provides some built-in concurrency primitives, like channel-based communication. Gobra is intended to verify such programs. Gobra is used in the VerifiedSCION and Centre for Cyber Trust projects to verify correctness and security properties of substantial codebases. The Gobra project is open-source and available on external pageGithub. There is also a external pageZulip organization for discussions related to Gobra.
Links
external pageGitHub pages
external pageZulip channel
Gobra versions of the examples and exercises from Rustan Leino's book external pageProgram Proofs
Project Members
Linard Arquint
João Carlos Mendes Pereira
Peter Müller
Dionisios Spiliopoulos
Felix Wolf
Nicolas Klose
Malte Schwerhoff
Publications
- F. A. Wolf and L. Arquint and M. Clochard and W. Oortwijn and J. C. Pereira and P. Müller: Gobra: Modular Specification and Verification of Go Programs
In Computer Aided Verification (CAV), 2021. [PDF][BIB][external pagePublisher][external pageTalk] - F. A. Wolf and L. Arquint and M. Clochard and W. Oortwijn and J. C. Pereira and P. Müller: Gobra: Modular Specification and Verification of Go Programs (extended version)
In arXiv, 2021. [external pagearXiv]