Title :
VERMEER: A Tool for Tracing and Explaining Faulty C Programs
Author :
Schwartz-Narbonne, Daniel ; Chanseok Oh ; Schaf, Martin ; Wies, Thomas
Abstract :
We present VERMEER, a new automated debugging tool for C. VERMEER 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 explains why the trace fails. The tool works in phases that simplify the input program to a linear trace, which is then analyzed using an automated theorem prover to produce the explanation. The output of each phase is a valid C program. VERMEER is able to produce useful explanations of non trivial traces for real C programs within a few seconds. The tool demo can be found at http://youtu.be/E5lKHNJVerU.
Keywords :
C language; program debugging; program diagnostics; software tools; theorem proving; VERMEER; automated debugging tool; automated theorem prover; dynamic tracer; faulty C program tracing; linearized trace; static analyzer; Algorithm design and analysis; Benchmark testing; Concrete; Debugging; Interpolation; Libraries; Software;
Conference_Titel :
Software Engineering (ICSE), 2015 IEEE/ACM 37th IEEE International Conference on
Conference_Location :
Florence
DOI :
10.1109/ICSE.2015.236
