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.

Finding Software Vulnerabilities by Test-Case Generation of C Programs

Map2Check is a software verification tool to check for safety properties about 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.

Image from https://doi.org/10.1007/s10009-016-0426-1

MetaSMT

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.

CRAB-LLVM

Our tool adopts Crab-LLVM is a static analyzer that computes inductive invariants for LLVM-based languages based on the Crab library.

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.