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:
For installation and usage, please follow the instructions in the README file.
Chanseok Oh, Martin Schäf, Daniel-Schwartz-Narbonne, and Thomas Wies. In ICSE, Demonstrations Track, 2015
Chanseok Oh, Martin Schäf, Daniel-Schwartz-Narbonne, and Thomas Wies. In SCAM 2014.
Jürgen Christ, Evren Ermis, Martin Schäf, and Thomas Wies. In VMCAI 2013.
Evren Ermis, Martin Schäf, and Thomas Wies. In FM 2012.
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.