Map2Check: Using Symbolic Execution and Fuzzing

Herbert Rocha, Rafael Menezes, Lucas Cordeiro, Raimundo Barreto

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


Map2Check is a software verification tool that combines fuzzing, symbolic execution, and inductive invariants. It automatically checks safety properties in C programs by adopting source code instrumentation to monitor data (e.g., memory pointers) from the program’s executions using LLVM compiler infrastructure. For SV-COMP 2020, we extended Map2Check to exploit an iterative deepening approach using LibFuzzer and Klee to check for safety properties. We also use Crab-LLVM to infer program invariants based on reachability analysis. Experimental results show that Map2Check can handle a wide variety of safety properties in several intricate verification tasks from SV-COMP 2020.
Original languageEnglish
Title of host publication26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Publication statusAccepted/In press - 17 Feb 2020


Dive into the research topics of 'Map2Check: Using Symbolic Execution and Fuzzing'. Together they form a unique fingerprint.

Cite this