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.

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
C

Links

Last commit date

29 April 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_42 (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: Vajra (part of VeriAbs)

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.