Gobra

Logo

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 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 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]

Selected Publications using Gobra

  • 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 pagePublisher] [external pageTalk]

  • 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 pagePublisher]
JavaScript has been disabled in your browser