Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)

Rafael Menezes; Lucas Cordeiro; Raimundo Barreto; Herbert  Rocha

doi:10.1007/978-3-030-45237-7_29

Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)

Rafael Menezes, Lucas Cordeiro, Raimundo Barreto, Herbert Rocha

Federal University of Roraima

Research output: Contribution to conference › Paper › peer-review

Abstract

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 language	English
Pages	403-407
Number of pages	5
DOIs	https://doi.org/10.1007/978-3-030-45237-7_29
Publication status	Published - 2020

Access to Document

10.1007/978-3-030-45237-7_29

Cite this

@conference{672b95887e3d432a9602f352d2cb22e2,

title = "Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)",

abstract = "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{\textquoteright}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.",

author = "Rafael Menezes and Lucas Cordeiro and Raimundo Barreto and Herbert Rocha",

year = "2020",

doi = "10.1007/978-3-030-45237-7_29",

language = "English",

pages = "403--407",

}

TY - CONF

T1 - Map2Check: Using Symbolic Execution and Fuzzing

T2 - (Competition Contribution)

AU - Menezes, Rafael

AU - Cordeiro, Lucas

AU - Barreto, Raimundo

AU - Rocha, Herbert

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-45237-7_29

DO - 10.1007/978-3-030-45237-7_29

M3 - Paper

SP - 403

EP - 407

ER -

Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)

Abstract

Access to Document

Fingerprint

Cite this