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

• Separation logic
• Termination
• Concurrency
• Symbolic execution
• Deductive verification

Type of tool

Deductive verifier

Expected input

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

Format:

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.

Internals

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.

Comments

License: MIT