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

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.
C

Links

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

Last commit date

22 November 2017

Related papers

https://doi.org/10.1007/978-3-319-89963-3_27 (TACAS '18)

Last publication date

14 April 2018

ProVerB specific

View/edit source (Markdown)



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