PV4 Verifastchecks for illegal memory accesses, data races and user-written specifications in C/Java code

Separation logic-based modular verifier for C and Java programs.

Application domain/field

Type of tool

Deductive verifier

Expected input

Program annotated with preconditions, postconditions, etc. that express the expected behavior of the program


C or Java program. Specifications are written as comments in Verifast's own specification language.

Expected output

"0 errors found" or indicates the location of a potential error.


Verifast checks that the program does not perform illegal memory accesses, does not include data races and complies with the specified pre- and postconditions. Uses Z3.


License: MIT


Related papers

Last publication date

15 July 2021

Related tools

ProVerB specific

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