{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/29653"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/29653","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"A C/C++ front end for the Daikon dynamic invariant detection system","abstract":"This thesis details the implementation and performance of a Daikon front end for the C and C++ languages. The Daikon dynamic invariant detection suite is a system designed to extract formal specifications from programs, in the form of information about their variables and their relationships to each other. The system consists of a front end and the analysis engine. The front end instruments the source code of a target program, inserting code that outputs the values of the program's variables when run. The user compiles and runs the instrumented program, generating a trace file that contains variable values. 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 discover invariants that current static methods cannot find. 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 and 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.","abstract_html":"This thesis details the implementation and performance of a Daikon front end for the C and C++ languages. The Daikon dynamic invariant detection suite is a system designed to extract formal specifications from programs, in the form of information about their variables and their relationships to each other. The system consists of a front end and the analysis engine. The front end instruments the source code of a target program, inserting code that outputs the values of the program's variables when run. The user compiles and runs the instrumented program, generating a trace file that contains variable values. 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 discover invariants that current static methods cannot find. 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 and 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.","abstract_has_math":false,"creators":["Morse, Benjamin, 1979-"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Michael D. Ernst."],"committee_chairs":[],"committee_members":[],"year":2002,"date_issued":"2002","date_published":"2002","updated_at":"2026-07-22T22:20:56Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/29653","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Michael D. Ernst."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Morse, Benjamin, 1979-"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2006-03-24T16:12:07Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2006-03-24T16:12:07Z"]},{"key":"dc:date.issued","label":"Date","values":["2002"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/29653"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (M.Eng. and S.B.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2002.","Includes bibliographical references (p. 73-75)."]},{"key":"dc:description.abstract","label":"Abstract","values":["This thesis details the implementation and performance of a Daikon front end for the C and C++ languages. The Daikon dynamic invariant detection suite is a system designed to extract formal specifications from programs, in the form of information about their variables and their relationships to each other. The system consists of a front end and the analysis engine. The front end instruments the source code of a target program, inserting code that outputs the values of the program's variables when run. The user compiles and runs the instrumented program, generating a trace file that contains variable values. 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 discover invariants that current static methods cannot find. 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 and 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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M.Eng.and S.B."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["A C/C++ front end for the Daikon dynamic invariant detection system"]}]}],"canonical_facts":{"dc:contributor.advisor":["Michael D. Ernst."],"dc:contributor.department":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science."],"dc:creator":["Morse, Benjamin, 1979-"],"dc:date.accessioned":["2006-03-24T16:12:07Z"],"dc:date.available":["2006-03-24T16:12:07Z"],"dc:date.issued":["2002"],"dc:description":["Thesis (M.Eng. and S.B.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2002.","Includes bibliographical references (p. 73-75)."],"dc:description.abstract":["This thesis details the implementation and performance of a Daikon front end for the C and C++ languages. The Daikon dynamic invariant detection suite is a system designed to extract formal specifications from programs, in the form of information about their variables and their relationships to each other. The system consists of a front end and the analysis engine. The front end instruments the source code of a target program, inserting code that outputs the values of the program's variables when run. The user compiles and runs the instrumented program, generating a trace file that contains variable values. 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 discover invariants that current static methods cannot find. 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 and 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."],"dc:description.degree":["M.Eng.and S.B."],"dc:format.mimetype":["application/pdf"],"dc:identifier.uri":["http://hdl.handle.net/1721.1/29653"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["A C/C++ front end for the Daikon dynamic invariant detection system"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:20:56Z"}