About

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.

Demo

Download

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:

• Source code repository at GitHub

• Source code distribution (release date 11/21/14)

  For installation and usage, please follow the instructions in the README file.

People

The following people have contributed to Vermeer:

• Daniel Schwartz-Narbonne

• Andreas Holzer

• Chanseok Oh

• Martin Schäf

• Thomas Wies

Publications

• VERMEER: A Tool for Tracing and Explaining Faulty C Programs

  Chanseok Oh, Martin Schäf, Daniel-Schwartz-Narbonne, and Thomas Wies. In ICSE, Demonstrations Track, 2015

• Concolic Fault Abstraction

  Chanseok Oh, Martin Schäf, Daniel-Schwartz-Narbonne, and Thomas Wies. In SCAM 2014.

• Flow-Sensitive Fault Localization

  Jürgen Christ, Evren Ermis, Martin Schäf, and Thomas Wies. In VMCAI 2013.

• Error Invariants

  Evren Ermis, Martin Schäf, and Thomas Wies. In FM 2012.

Acknowledgments

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.