{"id":{"repo_id":"texas","oai_identifier":"oai:repositories.lib.utexas.edu:2152/46708"},"canonical_url":"https://search.dev.ndltd.org/etd/texas/oai:repositories.lib.utexas.edu:2152/46708","repository":{"repo_id":"texas","name":"University of Texas","base_url":"https://repositories.lib.utexas.edu/server/oai/request"},"display":{"title":"Design of Deryaft : a novel framework for generating representation invariants of structurally complex data","abstract":"This dissertation presents a novel approach for generating likely structural invariants of complex data structures. Generating likely invariants using dynamic analyses is becoming an increasingly effective technique in software checking methodologies. Given a small set of concrete structures, our approach analyzes their key characteristics to formulate local and global properties that the structures exhibit. For effective formulation of structural invariants, this approach focuses on graph properties, including reachability, and views the program heap as an edge-labeled graph. The Deryaft Tool implements this approach for Java. Deryaft outputs a Java predicate that represents the invariants; the predicate takes an input structure and returns true if and only if it satisfies the invariants. The invariants generated by Deryaft directly enable automation of various existing frameworks, such as the Korat test generation framework and the Juzi data structure repair framework, which otherwise require the user to provide the invariants. Experimental results with the Deryaft prototype show that it feasibly generates invariants for a range of subject structures, including libraries as well as a stand-alone application. The focus of this dissertation is design of Deryaft but we also provide details of aDeryaft which specializes our algorithm for Alloy constraint generation and facilitates frameworks such as TestEra for test generation.","abstract_html":"This dissertation presents a novel approach for generating likely structural invariants of complex data structures. Generating likely invariants using dynamic analyses is becoming an increasingly effective technique in software checking methodologies. Given a small set of concrete structures, our approach analyzes their key characteristics to formulate local and global properties that the structures exhibit. For effective formulation of structural invariants, this approach focuses on graph properties, including reachability, and views the program heap as an edge-labeled graph. The Deryaft Tool implements this approach for Java. Deryaft outputs a Java predicate that represents the invariants; the predicate takes an input structure and returns true if and only if it satisfies the invariants. The invariants generated by Deryaft directly enable automation of various existing frameworks, such as the Korat test generation framework and the Juzi data structure repair framework, which otherwise require the user to provide the invariants. Experimental results with the Deryaft prototype show that it feasibly generates invariants for a range of subject structures, including libraries as well as a stand-alone application. The focus of this dissertation is design of Deryaft but we also provide details of aDeryaft which specializes our algorithm for Alloy constraint generation and facilitates frameworks such as TestEra for test generation.","abstract_has_math":false,"creators":["Malik, Muhammad Zubair"],"institution":"University of Texas at Austin","degree_name":"Master of Science","degree_level":"Masters","degree_discipline":"Electrical and Computer Engineering","degree_department":null,"school":null,"contributors":[],"advisors":["Khurshid, Sarfraz"],"committee_chairs":[],"committee_members":[],"year":2007,"date_issued":"2007-12","date_published":"2007-12","updated_at":"2026-07-24T05:01:00Z","subjects":["Structural invariants","Complex data structures","Java programming language"],"languages":["eng"],"rights":["Copyright © is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["doi:10.15781/T2JM23N0R"],"render_values":[{"text":"doi:10.15781/T2JM23N0R","href":"https://doi.org/10.15781/T2JM23N0R","code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2152/46708","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Khurshid, Sarfraz"]},{"key":"dc:creator","label":"Author","values":["Malik, Muhammad Zubair"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2017-05-04T14:48:41Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2017-05-04T14:48:41Z"]},{"key":"dc:date.issued","label":"Date","values":["2007-12"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical and Computer Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Texas at Austin"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Structural invariants","Complex data structures","Java programming language"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright © is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["doi:10.15781/T2JM23N0R"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/2152/46708"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["This dissertation presents a novel approach for generating likely structural invariants of complex data structures. Generating likely invariants using dynamic analyses is becoming an increasingly effective technique in software checking methodologies. Given a small set of concrete structures, our approach analyzes their key characteristics to formulate local and global properties that the structures exhibit. For effective formulation of structural invariants, this approach focuses on graph properties, including reachability, and views the program heap as an edge-labeled graph. The Deryaft Tool implements this approach for Java. Deryaft outputs a Java predicate that represents the invariants; the predicate takes an input structure and returns true if and only if it satisfies the invariants. The invariants generated by Deryaft directly enable automation of various existing frameworks, such as the Korat test generation framework and the Juzi data structure repair framework, which otherwise require the user to provide the invariants. Experimental results with the Deryaft prototype show that it feasibly generates invariants for a range of subject structures, including libraries as well as a stand-alone application. The focus of this dissertation is design of Deryaft but we also provide details of aDeryaft which specializes our algorithm for Alloy constraint generation and facilitates frameworks such as TestEra for test generation."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["electronic"]},{"key":"dc:title","label":"Title","values":["Design of Deryaft : a novel framework for generating representation invariants of structurally complex data"]}]}],"canonical_facts":{"dc:contributor.advisor":["Khurshid, Sarfraz"],"dc:creator":["Malik, Muhammad Zubair"],"dc:date.accessioned":["2017-05-04T14:48:41Z"],"dc:date.available":["2017-05-04T14:48:41Z"],"dc:date.issued":["2007-12"],"dc:description.abstract":["This dissertation presents a novel approach for generating likely structural invariants of complex data structures. Generating likely invariants using dynamic analyses is becoming an increasingly effective technique in software checking methodologies. Given a small set of concrete structures, our approach analyzes their key characteristics to formulate local and global properties that the structures exhibit. For effective formulation of structural invariants, this approach focuses on graph properties, including reachability, and views the program heap as an edge-labeled graph. The Deryaft Tool implements this approach for Java. Deryaft outputs a Java predicate that represents the invariants; the predicate takes an input structure and returns true if and only if it satisfies the invariants. The invariants generated by Deryaft directly enable automation of various existing frameworks, such as the Korat test generation framework and the Juzi data structure repair framework, which otherwise require the user to provide the invariants. Experimental results with the Deryaft prototype show that it feasibly generates invariants for a range of subject structures, including libraries as well as a stand-alone application. The focus of this dissertation is design of Deryaft but we also provide details of aDeryaft which specializes our algorithm for Alloy constraint generation and facilitates frameworks such as TestEra for test generation."],"dc:format.medium":["electronic"],"dc:identifier":["doi:10.15781/T2JM23N0R"],"dc:identifier.uri":["http://hdl.handle.net/2152/46708"],"dc:language.iso":["eng"],"dc:rights":["Copyright © is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works."],"dc:subject":["Structural invariants","Complex data structures","Java programming language"],"dc:title":["Design of Deryaft : a novel framework for generating representation invariants of structurally complex data"],"dc:type":["Thesis"],"thesis:degree_discipline":["Electrical and Computer Engineering"],"thesis:degree_level":["Masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["University of Texas at Austin"]},"updated_at":"2026-07-24T05:01:00Z"}