Map2Check is a method of automatically generating and checking safety properties (e.g., Unreachability of Error Function, and Memory Safety) 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.
Our tool adopts American Fuzzy Lop as a compile-time instrumentation and genetic algorithms to automatically discover clean, interesting test cases that trigger new internal states in the targeted binary.
Map2Check has been participed in the Intl. Competition on Software Verification (SV-COMP) held at TACAS.
Our tool adopts MetaSMT to improve our solvers supported. MetaSMT is a wrapper around various SMT or SMT-like solvers. This means you are able to program against this library and use any of the implemented solvers.
Our tool adopts Crab-LLVM is a static analyzer that computes inductive invariants for LLVM-based languages based on the Crab library.
Map2Check tool have improved based on academic research, more details checkout Publications.