Automatic Test Generation

Map2Check is a method of automatically generating and checking memory management unit tests 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 Memory Management Test-Case Generation of C Programs

Map2Check checks for properties related to pointer safety, memory leaks, and invalid deallocation.

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.

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.