Map2Check Tool: Using Symbolic Execution and Fuzzing

Abstract

Map2Check is a software verification tool that automatically generating and checking safety properties in C programs. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. The generation of the test cases are based on assertions (safety properties) from the code instructions, adopting the LLVM framework version 6.0, LibFuzzer, KLEE to generate input values to the test cases generated by Map2Check. Additionally, we have adopted the Crab-LLVM tool to computes inductive invariants for LLVM-based languages. Experimental results show that Map2Check can handle a wide variety of safety properties in several intricate verification tasks from SV-COMP 2020.