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

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

Descripción completa

Detalles Bibliográficos
Autores principales: Rocha, Herbert, Menezes, Rafael, Cordeiro, Lucas C., Barreto, Raimundo
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480707/
http://dx.doi.org/10.1007/978-3-030-45237-7_29
_version_ 1783580463953084416
author Rocha, Herbert
Menezes, Rafael
Cordeiro, Lucas C.
Barreto, Raimundo
author_facet Rocha, Herbert
Menezes, Rafael
Cordeiro, Lucas C.
Barreto, Raimundo
author_sort Rocha, Herbert
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7480707
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74807072020-09-10 Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution) Rocha, Herbert Menezes, Rafael Cordeiro, Lucas C. Barreto, Raimundo Tools and Algorithms for the Construction and Analysis of Systems Article 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. 2020-03-13 /pmc/articles/PMC7480707/ http://dx.doi.org/10.1007/978-3-030-45237-7_29 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Rocha, Herbert
Menezes, Rafael
Cordeiro, Lucas C.
Barreto, Raimundo
Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)
title Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)
title_full Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)
title_fullStr Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)
title_full_unstemmed Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)
title_short Map2Check: Using Symbolic Execution and Fuzzing: (Competition Contribution)
title_sort map2check: using symbolic execution and fuzzing: (competition contribution)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480707/
http://dx.doi.org/10.1007/978-3-030-45237-7_29
work_keys_str_mv AT rochaherbert map2checkusingsymbolicexecutionandfuzzingcompetitioncontribution
AT menezesrafael map2checkusingsymbolicexecutionandfuzzingcompetitioncontribution
AT cordeirolucasc map2checkusingsymbolicexecutionandfuzzingcompetitioncontribution
AT barretoraimundo map2checkusingsymbolicexecutionandfuzzingcompetitioncontribution

Ejemplares similares