PV3 ⊧ Diffychecks user-specified assertions in a C programVerification technique to prove properties of a class of array programs with a symbolic parameter N denoting the size of the arrays.
- Array programs
- Program verification
Expected inputC program with assertions, arrays need to be stack allocated instead of malloc'd.
Format:C program: similar format to what is used for SV-COMP. Assertions are expressed as
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.