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.
Cite
CITATION STYLE
Menezes, R., Rocha, H., Cordeiro, L., & Barreto, R. (2018). Map2Check using LLVM and KLEE: (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10806 LNCS, pp. 437–441). Springer Verlag. https://doi.org/10.1007/978-3-319-89963-3_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
