Map2Check is a method of automatically generating and checking memory management unit tests in C programs.
Map2Check adopts source code instrumentation to monitor data from the program’s executions, aiming to verify the generated test cases and to detect failures originating from the safety properties of the analyzed program.
Map2Check is implemented as a source-to-source transformation tool adopting a collection of modular and reusable compiler and tool chain technologies, e.g., LLVM.
In this new version of Map2Check tool, we have been adopted LLVM as a compiler framework to improve our code instrumentation and optimizations.
Our tool adopts KLEE as a symbolic execution engine that is capable of automatically generating tests that achieve high coverage on a diverse set of complex programs.
Map2Check tool have improved based on academic research, more details checkout Publications.