PV3 Diffychecks user-specified assertions in a C program

Verification technique to prove properties of a class of array programs with a symbolic parameter N denoting the size of the arrays.

Application domain/field

Expected input

C program with assertions, arrays need to be stack allocated instead of malloc'd.


C program: similar format to what is used for SV-COMP. Assertions are expressed as __VERIFIER_assert(...)

Expected output

DIFFY_VERIFICATION_SUCCESSFUL when the given post-condition is verified. DIFFY_VERIFICATION_FAILED when the given post-condition is violated. DIFFY_VERIFICATION_UNKNOWN when the result cannot be determined.


Uses Z3.


License: MIT


Related papers

Diffy: Inductive Reasoning of Array Programs Using Difference Invariants (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: Vajra (part of VeriAbs)

ProVerB specific

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