Gobra: Modular Specification and Verification of Go Programs

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 correctness and security properties of such programs, scaling to substantial codebases.

Read More #

• Visit our project website!
• Gobra’s initial publication is available here.
• Gobra is open-source. You find the code here.

Project Members #

• Linard Arquint (ETH Zurich)
• João Carlos Mendes Pereira (ETH Zurich)
• Peter Müller (ETH Zurich)
• Nicolas Ray Klose (ETH Zurich)
• Malte Schwerhoff (ETH Zurich)
• Dionisios Spiliopoulos (ETH Zurich)
• Felix Wolf (ETH Zurich)