Translating alloy using Boolean circuits
Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2006
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/33129 |
| _version_ | 1811079465482059776 |
|---|---|
| author | Daitch, Samuel Isaac |
| author2 | Daniel Jackson. |
| author_facet | Daniel Jackson. Daitch, Samuel Isaac |
| author_sort | Daitch, Samuel Isaac |
| collection | MIT |
| description | Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004. |
| first_indexed | 2024-09-23T11:15:27Z |
| format | Thesis |
| id | mit-1721.1/33129 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T11:15:27Z |
| publishDate | 2006 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/331292019-04-11T14:09:27Z Translating alloy using Boolean circuits Daitch, Samuel Isaac Daniel 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 (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004. Includes bibliographical references (p. 71-72). Alloy is a automatically analyzable modelling language based on first-order logic. An Alloy model can be translated into a Boolean formula whose satisfying assignments correspond to instances in the model. Currently, the translation procedure mechanically converts each piece of the Alloy model individually into its most straightforward Boolean representation. This thesis proposes a more efficient approach to translating Alloy models. The key is to take advantage of the fact that an Alloy model contains patterns that are used repeatedly. This makes it natural to give a model a more structured Boolean representation, namely a Boolean circuit. Reusable pieces in the model correspond to circuit components. By identifying the most frequently used components and optimizing their corresponding Boolean formulas, the size of the overall formula for the model would be reduced without significant additional work. A smaller formula would potentially decrease the time required to determine satisfiability, resulting in faster analysis overall. by Samuel Isaac Daitch. M.Eng. 2006-06-19T17:43:57Z 2006-06-19T17:43:57Z 2004 2004 Thesis http://hdl.handle.net/1721.1/33129 62241194 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 72 p. 2516311 bytes 2519005 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Daitch, Samuel Isaac Translating alloy using Boolean circuits |
| title | Translating alloy using Boolean circuits |
| title_full | Translating alloy using Boolean circuits |
| title_fullStr | Translating alloy using Boolean circuits |
| title_full_unstemmed | Translating alloy using Boolean circuits |
| title_short | Translating alloy using Boolean circuits |
| title_sort | translating alloy using boolean circuits |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/33129 |
| work_keys_str_mv | AT daitchsamuelisaac translatingalloyusingbooleancircuits |