Core extraction and non-example generation : debugging and understanding logical models
Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, June 2005.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2006
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/34127 |
| _version_ | 1826203661833863168 |
|---|---|
| author | Seater, Robert Morrison |
| author2 | Daniel N. Jackson. |
| author_facet | Daniel N. Jackson. Seater, Robert Morrison |
| author_sort | Seater, Robert Morrison |
| collection | MIT |
| description | Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, June 2005. |
| first_indexed | 2024-09-23T12:41:06Z |
| format | Thesis |
| id | mit-1721.1/34127 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T12:41:06Z |
| publishDate | 2006 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/341272019-04-14T07:48:47Z Core extraction and non-example generation : debugging and understanding logical models Seater, Robert Morrison Daniel N. Jackson. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, June 2005. Includes bibliographical references (p. 127-132). 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. by Robert Morrison Seater. S.M. 2006-09-28T15:05:51Z 2006-09-28T15:05:51Z 2004 2005 Thesis http://hdl.handle.net/1721.1/34127 67767132 eng 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. http://dspace.mit.edu/handle/1721.1/7582 132 p. 5800043 bytes 5805546 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Seater, Robert Morrison Core extraction and non-example generation : debugging and understanding logical models |
| title | Core extraction and non-example generation : debugging and understanding logical models |
| title_full | Core extraction and non-example generation : debugging and understanding logical models |
| title_fullStr | Core extraction and non-example generation : debugging and understanding logical models |
| title_full_unstemmed | Core extraction and non-example generation : debugging and understanding logical models |
| title_short | Core extraction and non-example generation : debugging and understanding logical models |
| title_sort | core extraction and non example generation debugging and understanding logical models |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/34127 |
| work_keys_str_mv | AT seaterrobertmorrison coreextractionandnonexamplegenerationdebuggingandunderstandinglogicalmodels |