Declarative symbolic pure-logic model checking
Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2005.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2006
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/30184 |
| _version_ | 1811096396081659904 |
|---|---|
| author | Shlyakhter, Ilya, 1975- |
| author2 | Daniel N. Jackson. |
| author_facet | Daniel N. Jackson. Shlyakhter, Ilya, 1975- |
| author_sort | Shlyakhter, Ilya, 1975- |
| collection | MIT |
| description | Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2005. |
| first_indexed | 2024-09-23T16:42:46Z |
| format | Thesis |
| id | mit-1721.1/30184 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T16:42:46Z |
| publishDate | 2006 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/301842019-04-11T01:15:17Z Declarative symbolic pure-logic model checking Shlyakhter, Ilya, 1975- 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, 2005. Includes bibliographical references (p. 173-181). Model checking, a technique for findings errors in systems, involves building a formal model that describes possible system behaviors and correctness conditions, and using a tool to search for model behaviors violating correctness properties. Existing model checkers are well-suited for analyzing control-intensive algorithms (e.g. network protocols with simple node state). Many important analyses, however, fall outside the capabilities of existing model checkers. Examples include checking algorithms with complex state, distributed algorithms over all network topologies, and highly declarative models. This thesis addresses the problem of building an efficient model checker that overcomes these limitations. The work builds on Alloy, a relational modeling language. Previous work has defined the language and shown that it can be analyzed by translation to SAT. The primary contributions of this thesis include: a modeling paradigm for describing complex structures in Alloy; significant improvements in scalability of the analyzer; and improvements in usability of the analyzer via addition of a debugger for over constraints. Together, these changes make model-checking practical for important new classes of analyses. While the work was done in the context of Alloy, some techniques generalize to other verification tools. by Ilya A. Shlyakhter. S.M. 2006-03-24T18:27:33Z 2006-03-24T18:27:33Z 2005 2005 Thesis http://hdl.handle.net/1721.1/30184 60680023 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 181 p. 9773619 bytes 9796412 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Shlyakhter, Ilya, 1975- Declarative symbolic pure-logic model checking |
| title | Declarative symbolic pure-logic model checking |
| title_full | Declarative symbolic pure-logic model checking |
| title_fullStr | Declarative symbolic pure-logic model checking |
| title_full_unstemmed | Declarative symbolic pure-logic model checking |
| title_short | Declarative symbolic pure-logic model checking |
| title_sort | declarative symbolic pure logic model checking |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/30184 |
| work_keys_str_mv | AT shlyakhterilya1975 declarativesymbolicpurelogicmodelchecking |