PV4 Gobrachecks memory safety, crash safety, data-race freedom, and user-provided specifications for Go programs

Deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications.

Application domain/field

Type of tool

Deductive program verifier

Expected input

Go program with specifications

Format:

.gobra file Specifications should be written in the form of assertions (preconditions, postconditions, loop invariants, predicates) in the program code.

Expected output

If verification fails, then it will report on the level of the Go program, what assertions could not be proven.

Internals

Gobra takes an annotated Go program as input. It will then encode this annotated program into the intermediate verification language Viper and apply an existing SMT-based verifier. If verification fails, then it will report on the level of the Go program, what assertions could not be proven.

Comments

License: Mozilla Public License version 2.0 with exceptions for some files.
Go

Links

Related papers

Gobra: Modular Specification and Verification of Go Programs (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.