PV3 VIAP (Verifier for Integer Assignment Programs)checks user-provided assertions in C programs

an automated system for verifying safety properties of procedural programs with integer assignments and loops

Application domain/field

Type of tool

Monoverifier

Expected input

C program with user-provided assertions

Format:

C99

Expected output

TRUE (safe) / FALSE (counterexample produced) / UNKNOWN (otherwise)

Internals

C is translated to a set of first order axioms SymPy is used as an algebraic simplifier Z3 as a theorem prover tries to prove postconditions
C

Links

Last commit date

6 Apr 2019

Related papers

Last publication date

4 Apr 2019

ProVerB specific

View/edit source (Markdown)



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