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 verifierExpected input
Go program with specificationsFormat:
.gobra
file
Specifications should be written in the form of assertions (preconditions, postconditions, loop invariants, predicates) in the program code.