Hunting Memory Bugs in C Programs with Map2Check

Herbert O. Rocha, Raimundo S. Barreto, Lucas C. Cordeiro

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


Map2Check is a tool for automatically generating and checking unit tests for C programs. The generation of unit tests is based on assertions extracted from (memory) safety properties, which are generated by the ESBMC tool. In particular, Map2Check checks for SV-COMP invalid-free, invalid-dereference, and memory-leak properties in C programs.
Original languageEnglish
Title of host publication Algorithms for the Construction and Analysis of Systems ( TACAS 2016)
Publication statusPublished - 2016

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'Hunting Memory Bugs in C Programs with Map2Check'. Together they form a unique fingerprint.

Cite this