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

• Array programs
• Program verification
• Invariants

Expected input

C 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 __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.

Internals

Uses Z3.

Comments

License: MIT