PV1 InterpCheckerchecks whether unsafe states in C code can be reached

InterpChecker is a tool for verifying safety properties of C programs

Application domain/field

Type of tool

Model checker?

Expected input

C program instrumented with error labels


.c file

Expected output

UNSAFE or SAFE indicating whether the program can reach unsafe states (i.e. error labels)


Implementation builds on CPAchecker. Given a C program, it will use reachability checking to see whether it can reach any of the instrumented error labels.


False negatives may occur for programs with recursive functions since recursive functions are treated as pure functions.


Repository: https://github.com/duanzhao-dz/interpchecker

Related papers

InterpChecker: Reducing State Space via Interpolations (TACAS '18)

Last publication date

14 April 2018

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.