Map2Check using LLVM and KLEE: (Competition contribution)

Rafael Menezes, Herbert Rocha, Lucas Cordeiro, Raimundo Barreto

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

Abstract

Map2Check is a bug hunting tool that automatically checks safety properties in C programs. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. Here, we extend Map2Check to: (i) simplify the program using Clang/LLVM; (ii) perform a path-based symbolic execution using the KLEE tool; and (iii) transform and instrument the code using the LLVM dynamic information flow. The SVCOMP’18 results show that Map2Check can be effective in generating and checking test cases related to memory management of C programs.
Original languageEnglish
Title of host publicationTOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT II
Pages437-441
Number of pages5
Volume10806
DOIs
Publication statusPublished - 2018

Publication series

NameLecture Notes in Computer Science

Fingerprint

Dive into the research topics of 'Map2Check using LLVM and KLEE: (Competition contribution)'. Together they form a unique fingerprint.

Cite this