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

• Deductive verification
• Memory safety
• Data-race freedom
• Functional correctness
• Separation logic

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.