Vermeer - An Automated Debugging Tool for C


Vermeer is an automated debugging tool for ANSI-C programs. It combines two functionalities: (1) a dynamic tracer that produces a linearized trace from a faulty C program and a given test input; and (2) a static analyzer that produces an explanation why the trace fails. The tool works in phases that gradually simplify the input program to a linear trace, which is then analyzed using an automated theorem prover to produce the explanation. Each analysis phase produces an executable C program. This maximizes the ease of interaction with the programmer and yields high interoperability with other analysis tools. Vermeer is able to produce useful explanations of non trivial error traces for real-world C programs within a few seconds.



Vermeer is implemented in OCaml on top of the C program analysis framework CIL. The tool is distributed as a source tarball under a BSD license:


The following people have contributed to Vermeer:



This material is based in part upon work supported by the National Science Foundation under grant CCF-1350574. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.