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

Last commit date

13 December 2021

Related papers

https://doi.org/10.1007/978-3-030-81685-8_17 (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.