Download: PDF, PostScript.
“A C/C++ Front End for the Daikon Dynamic Invariant Detection System” by Benjamin Morse. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), Aug. 2002.
The Daikon dynamic invariant detection suite is a system designed to extract specifications from programs, in the form of information about their variables and their relationships to each other. It does this by instrumenting the source code of a target program, which inserts code that directs the program to output the values of its variables and other information when run. This data is then sent to Daikon proper, which performs analysis on it and reports invariants about the program variables. Daikon is a useful tool that can suggest invariants beyond those provable by current static methods.
While the invariant analysis tool is language independent, the front ends — tools that instrument of the user code — must be written for every language to be instrumented. There is a huge base of pre-existing code written in C/C++ for which invariants can be discovered. C/C++ are also widely deployed, comprise a large segment of software currently in development, and are therefore valuable candidates for analysis. The key difficulty in instrumenting a type-unsafe language like C is that the instrumented program has to determine what variables are valid, and to what extent, so that it does not output garbage values or cause a segmentation fault by dereferencing an invalid pointer. This thesis details the implementation and performance of a Daikon front end for the C and C++ languages.
Download: PDF, PostScript.
BibTeX entry:
@mastersthesis{Morse02,
author = {Benjamin Morse},
title = {A {C/C++} Front End for the {Daikon} Dynamic Invariant
Detection System},
school = {MIT Department of Electrical Engineering and Computer Science},
address = {Cambridge, MA},
month = aug,
year = {2002}
}
(This webpage was created with bibtex2web.)
Back to Program Analysis Group publications.