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 pageGithubcall_made. There is also a external pageZulip organizationcall_made for discussions related to Gobra.
Links
external pageGitHub pagescall_made
external pageZulip channelcall_made
Gobra versions of the examples and exercises from Rustan Leino's book external pageProgram Proofscall_made
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 pagePublishercall_made][external pageTalkcall_made] - 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 pagearXivcall_made]