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 page Github. There is also a external page Zulip organization for discussions related to Gobra.
Links
external page GitHub pages
external page Zulip channel
Gobra versions of the examples and exercises from Rustan Leino's book external page Program Proofs
Project Members
Linard Arquint
João Carlos Mendes Pereira
Peter Müller
Dionisios Spiliopoulos
Felix Wolf
Nicolas Klose
Malte Schwerhoff
Publications on Gobra
- 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 page Publisher][external page Talk] - 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 page arXiv]
Selected Publications using Gobra
- J. C. Pereira, T. Klenze, S. Giampietro, M. Limbeck, D. Spiliopoulos, F. A. Wolf, M. Eilers, C. Sprenger, D. Basin, P. Müller, and A. Perrig: Protocols to Code: Formal Verification of a Next-Generation Internet Router
Technical Report, 2024. [PDF] [BIB] [external page arXiv]
- L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. N. Wiesner, D. Basin, and P. Müller: Sound Verification of Security Protocols: From Design to Interoperable Implementations
In 2023 IEEE Symposium on Security and Privacy (SP), 2023. [PDF] [BIB] [external page Publisher] [external page Talk]
- L. Arquint, M. Schwerhoff, V. Mehta, and P. Müller: A Generic Methodology for the Modular Verification of Security Protocol Implementations
In Computer and Communications Security (CCS), 2023. [PDF] [BIB] [external page Publisher]