{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/34127"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/34127","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Core extraction and non-example generation : debugging and understanding logical models","abstract":"Declarative models, in which conjunction and negation are freely used, are a powerful tool for software specification and verification. Unfortunately, tool support for developing and debugging such models is limited. The challenges to developing such tools are twofold: technical information must be extracted from the model, then that information must be presented to the user in way that is both meaningful and manageable. This document introduces two such techniques to help fill the gap. Non-example generation allows the user to ask for the role of a particular subformula in a model. A formula's role is explained in terms of how the set of satisfying solutions to the model would change were that subformula removed or altered. Core extraction helps detect and localize unintentional overconstraint, in which real counterexamples are masked by bugs in the model. It leverages recent advances in SAT solvers to identify irrelevant portions of an unsatisfiable model. Experiences are reported from applying these two techniques to a variety of existing models.","abstract_html":"Declarative models, in which conjunction and negation are freely used, are a powerful tool for software specification and verification. Unfortunately, tool support for developing and debugging such models is limited. The challenges to developing such tools are twofold: technical information must be extracted from the model, then that information must be presented to the user in way that is both meaningful and manageable. This document introduces two such techniques to help fill the gap. Non-example generation allows the user to ask for the role of a particular subformula in a model. A formula's role is explained in terms of how the set of satisfying solutions to the model would change were that subformula removed or altered. Core extraction helps detect and localize unintentional overconstraint, in which real counterexamples are masked by bugs in the model. It leverages recent advances in SAT solvers to identify irrelevant portions of an unsatisfiable model. Experiences are reported from applying these two techniques to a variety of existing models.","abstract_has_math":false,"creators":["Seater, Robert Morrison"],"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":["Daniel N. Jackson."],"committee_chairs":[],"committee_members":[],"year":2005,"date_issued":"2005","date_published":"2005","updated_at":"2026-07-22T22:21:40Z","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/34127","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Daniel N. Jackson."]},{"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":["Seater, Robert Morrison"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2006-09-28T15:05:51Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2006-09-28T15:05:51Z"]},{"key":"dc:date.issued","label":"Date","values":["2005"]},{"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/34127"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, June 2005.","Includes bibliographical references (p. 127-132)."]},{"key":"dc:description.abstract","label":"Abstract","values":["Declarative models, in which conjunction and negation are freely used, are a powerful tool for software specification and verification. Unfortunately, tool support for developing and debugging such models is limited. The challenges to developing such tools are twofold: technical information must be extracted from the model, then that information must be presented to the user in way that is both meaningful and manageable. This document introduces two such techniques to help fill the gap. Non-example generation allows the user to ask for the role of a particular subformula in a model. A formula's role is explained in terms of how the set of satisfying solutions to the model would change were that subformula removed or altered. Core extraction helps detect and localize unintentional overconstraint, in which real counterexamples are masked by bugs in the model. It leverages recent advances in SAT solvers to identify irrelevant portions of an unsatisfiable model. Experiences are reported from applying these two techniques to a variety of existing models."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Core extraction and non-example generation : debugging and understanding logical models"]}]}],"canonical_facts":{"dc:contributor.advisor":["Daniel N. Jackson."],"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":["Seater, Robert Morrison"],"dc:date.accessioned":["2006-09-28T15:05:51Z"],"dc:date.available":["2006-09-28T15:05:51Z"],"dc:date.issued":["2005"],"dc:description":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, June 2005.","Includes bibliographical references (p. 127-132)."],"dc:description.abstract":["Declarative models, in which conjunction and negation are freely used, are a powerful tool for software specification and verification. Unfortunately, tool support for developing and debugging such models is limited. The challenges to developing such tools are twofold: technical information must be extracted from the model, then that information must be presented to the user in way that is both meaningful and manageable. This document introduces two such techniques to help fill the gap. Non-example generation allows the user to ask for the role of a particular subformula in a model. A formula's role is explained in terms of how the set of satisfying solutions to the model would change were that subformula removed or altered. Core extraction helps detect and localize unintentional overconstraint, in which real counterexamples are masked by bugs in the model. It leverages recent advances in SAT solvers to identify irrelevant portions of an unsatisfiable model. Experiences are reported from applying these two techniques to a variety of existing models."],"dc:description.degree":["S.M."],"dc:format.mimetype":["application/pdf"],"dc:identifier.uri":["http://hdl.handle.net/1721.1/34127"],"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":["Core extraction and non-example generation : debugging and understanding logical models"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:21:40Z"}