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

• Recurrence solving
• Safety verification

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