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

• Safety verification
• Model checking
• Counterexample-guided abstraction refinement (CEGAR)
• Reachability checking

Type of tool

Model checker?

Expected input

C program instrumented with error labels

Format:

.c file

Expected output

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

Internals

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.

Comments

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