{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/42281"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/42281","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Improved software verification through program path-based analysis","abstract":"This thesis describes the generation and use of program invariants to improve software reliability. It introduces PRECIS, a technique for automatic invariant generation based on program path guided clustering. The invariants generated by PRECIS can be directly used by programmers for regression testing and improved code documentation. The generated invariants can also be used as part of hardware error detectors, by checking variables key to program output. PREAMBL, a bug localization technique, is introduced as away of providing increased utility to the generated invariants in diagnosing post-release bugs. The benefi ts of these uses of the generated invariants are shown through experiments. The high control-flow coverage of generated invariants is demonstrated for the Siemens benchmark suite, and higher quality is indicated when compared with Daikon, a prior technique. Fault injection experiments show high error detection coverage for several types of manifested errors. Results for PREAMBL show higher scoring for localized paths than previous approaches.","abstract_html":"This thesis describes the generation and use of program invariants to improve software reliability. It introduces PRECIS, a technique for automatic invariant generation based on program path guided clustering. The invariants generated by PRECIS can be directly used by programmers for regression testing and improved code documentation. The generated invariants can also be used as part of hardware error detectors, by checking variables key to program output. PREAMBL, a bug localization technique, is introduced as away of providing increased utility to the generated invariants in diagnosing post-release bugs. The benefi ts of these uses of the generated invariants are shown through experiments. The high control-flow coverage of generated invariants is demonstrated for the Siemens benchmark suite, and higher quality is indicated when compared with Daikon, a prior technique. Fault injection experiments show high error detection coverage for several types of manifested errors. Results for PREAMBL show higher scoring for localized paths than previous approaches.","abstract_has_math":false,"creators":["Sagdeo, Parth"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Vasudevan, Shobha"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2013,"date_issued":"2013-02-03T19:30:11Z","date_published":"2013-02-03T19:30:11Z","updated_at":"2026-07-22T22:25:33Z","subjects":["Fault Detection","Fault Tolerance","Bug Localization","Software Maintenance","Software Reliability","Invariant Generation","Assertion Generation"],"languages":["en"],"rights":["Copyright 2012 Parth Vivek Sagdeo"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/42281","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Vasudevan, Shobha"]},{"key":"dc:creator","label":"Author","values":["Sagdeo, Parth"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2013-02-03T19:30:11Z","2012-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Fault Detection","Fault Tolerance","Bug Localization","Software Maintenance","Software Reliability","Invariant Generation","Assertion Generation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2012 Parth Vivek Sagdeo"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/42281"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This thesis describes the generation and use of program invariants to improve software reliability. It introduces PRECIS, a technique for automatic invariant generation based on program path guided clustering. The invariants generated by PRECIS can be directly used by programmers for regression testing and improved code documentation. The generated invariants can also be used as part of hardware error detectors, by checking variables key to program output. PREAMBL, a bug localization technique, is introduced as away of providing increased utility to the generated invariants in diagnosing post-release bugs. The benefi ts of these uses of the generated invariants are shown through experiments. The high control-flow coverage of generated invariants is demonstrated for the Siemens benchmark suite, and higher quality is indicated when compared with Daikon, a prior technique. Fault injection experiments show high error detection coverage for several types of manifested errors. Results for PREAMBL show higher scoring for localized paths than previous approaches.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-12-12T16:55:22Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 Thesis.zip: 5212419 bytes, checksum: 70ec7cfb2ffb177b4e2811c3fcb2244d (MD5) ecethesis.pdf: 2329846 bytes, checksum: a0c92d3f75a297affd1821c833bf27ed (MD5)","Made available in DSpace on 2013-02-03T19:30:11Z (GMT). No. of bitstreams: 3 Parth_Sagdeo.pdf: 2329846 bytes, checksum: a0c92d3f75a297affd1821c833bf27ed (MD5) Thesis.zip: 5212419 bytes, checksum: 70ec7cfb2ffb177b4e2811c3fcb2244d (MD5) license.txt: 4058 bytes, checksum: af472f827d6ff7d53650aee1f2813bec (MD5)"]},{"key":"dc:title","label":"Title","values":["Improved software verification through program path-based analysis"]}]}],"canonical_facts":{"dc:contributor":["Vasudevan, Shobha"],"dc:creator":["Sagdeo, Parth"],"dc:date":["2013-02-03T19:30:11Z","2012-12"],"dc:description":["This thesis describes the generation and use of program invariants to improve software reliability. It introduces PRECIS, a technique for automatic invariant generation based on program path guided clustering. The invariants generated by PRECIS can be directly used by programmers for regression testing and improved code documentation. The generated invariants can also be used as part of hardware error detectors, by checking variables key to program output. PREAMBL, a bug localization technique, is introduced as away of providing increased utility to the generated invariants in diagnosing post-release bugs. The benefi ts of these uses of the generated invariants are shown through experiments. The high control-flow coverage of generated invariants is demonstrated for the Siemens benchmark suite, and higher quality is indicated when compared with Daikon, a prior technique. Fault injection experiments show high error detection coverage for several types of manifested errors. Results for PREAMBL show higher scoring for localized paths than previous approaches.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-12-12T16:55:22Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 Thesis.zip: 5212419 bytes, checksum: 70ec7cfb2ffb177b4e2811c3fcb2244d (MD5) ecethesis.pdf: 2329846 bytes, checksum: a0c92d3f75a297affd1821c833bf27ed (MD5)","Made available in DSpace on 2013-02-03T19:30:11Z (GMT). No. of bitstreams: 3 Parth_Sagdeo.pdf: 2329846 bytes, checksum: a0c92d3f75a297affd1821c833bf27ed (MD5) Thesis.zip: 5212419 bytes, checksum: 70ec7cfb2ffb177b4e2811c3fcb2244d (MD5) license.txt: 4058 bytes, checksum: af472f827d6ff7d53650aee1f2813bec (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/42281"],"dc:language":["en"],"dc:rights":["Copyright 2012 Parth Vivek Sagdeo"],"dc:subject":["Fault Detection","Fault Tolerance","Bug Localization","Software Maintenance","Software Reliability","Invariant Generation","Assertion Generation"],"dc:title":["Improved software verification through program path-based analysis"],"dc:type":["text"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:33Z"}