PV4 Map2Checkchecks user-specified properties, overflows and memory-safety of C programs

Map2Check is a bug hunting tool that automatically checks safety properties in C programs

Application domain/field

Expected input


Expected output

TRUE + witness, FALSE or FALSE(p) + witness or UNKNOWN. FALSE(p) means that the property p is violated.


Map2Check checks for the following (SV-COMP) properties: Uses KLEE, LibFuzzer, Crab-LLVM


License: GPL v2.0


Related papers

Last publication date

17 April 2020

Related tools

Other tools that participated in similar categories of SV-COMP: CPAchecker, DIVINE, ESBMC, PeSCo, Pinaka, Symbiotic, Ultimate Automizer, UKojak, VeriAbs, VeriFuzz

ProVerB specific

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