Automatic Test Generation

Map2Check is a method of automatically generating and checking safety properties (e.g., Unreachability of Error Function, and Memory Safety) in C programs.

Analysing C source code

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.

Architecture, Implementation and Availability

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.

A Test-Case Generation of C Programs

Map2Check checks for properties related to pointer safety, memory leaks, invalid deallocation, overflows, and unreachability of error location.

LLVM Compiler Infrastructure

In this new version of Map2Check tool, we have been adopted LLVM as a compiler framework to improve our code instrumentation and optimizations.

KLEE LLVM Execution Engine

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.

AFL FUzzer

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.

SV-COMP

Map2Check has been participed in the Intl. Competition on Software Verification (SV-COMP) held at TACAS.

Searching for Contributions

We have new plans to keep improving Map2Check tool, but if you have new ideas, please tell us.

Research

Map2Check tool have improved based on academic research, more details checkout Publications.