PV4 ⊧ Verifastchecks for illegal memory accesses, data races and user-written specifications in C/Java codeSeparation logic-based modular verifier for C and Java programs.
- Separation logic
- Symbolic execution
- Deductive verification
Type of toolDeductive verifier
Expected inputProgram 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.