The Hob system for verifying software design properties
Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2007
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/38688 |
| _version_ | 1826198158074445824 |
|---|---|
| author | Lam, Patrick, Ph. D. Massachusetts Institute of Technology |
| author2 | Martin Rinard. |
| author_facet | Martin Rinard. Lam, Patrick, Ph. D. Massachusetts Institute of Technology |
| author_sort | Lam, Patrick, Ph. D. Massachusetts Institute of Technology |
| collection | MIT |
| description | Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007. |
| first_indexed | 2024-09-23T11:00:06Z |
| format | Thesis |
| id | mit-1721.1/38688 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T11:00:06Z |
| publishDate | 2007 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/386882019-04-12T22:13:45Z The Hob system for verifying software design properties Lam, Patrick, Ph. D. Massachusetts Institute of Technology Martin Rinard. 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 (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2007. Includes bibliographical references (p. 157-164). This dissertation introduces novel techniques for verifying that programs conform to their designs. My Hob system, as described in this dissertation, allows developers to statically ensure that implementations preserve certain specified properties. Hob verifies heap-based properties that can express important aspects of a program's design. The key insight behind my approach is that Hob can establish detailed software design properties--properties that lie beyond the reach of extant static analysis techniques due to scalability or precision issues-by focusing the verification task. In particular, the Hob approach applies scalable static analysis techniques to the majority of the modules of a program and very precise, unscalable, static analysis or automated theorem proving techniques to certain specific modules of that program: those that require the precision that such analyses can deliver. The use of assume/guarantee reasoning allows the analysis engine to harness the strengths of both scalable and precise static analysis techniques to analyze large programs (which would otherwise require scalable, imprecise analyses) with sufficient precision to establish detailed data structure consistency properties, e.g. heap shape properties. (cont.) A set-based specification language enables the different analysis techniques to cooperate in verifying the specified design properties. My preliminary results show that it is possible to successfully verify detailed design-level properties of benchmark applications: I have used the Hob system to verify user-relevant properties of a water molecule simulator, a web server, and a minesweeper game. These properties constrain the behaviour of the program by stating that selected sets of objects are always equal or disjoint throughout the program's execution. by Patrick Lam. Ph.D. 2007-08-29T20:45:09Z 2007-08-29T20:45:09Z 2007 2007 Thesis http://hdl.handle.net/1721.1/38688 164437618 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 164 p. application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Lam, Patrick, Ph. D. Massachusetts Institute of Technology The Hob system for verifying software design properties |
| title | The Hob system for verifying software design properties |
| title_full | The Hob system for verifying software design properties |
| title_fullStr | The Hob system for verifying software design properties |
| title_full_unstemmed | The Hob system for verifying software design properties |
| title_short | The Hob system for verifying software design properties |
| title_sort | hob system for verifying software design properties |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/38688 |
| work_keys_str_mv | AT lampatrickphdmassachusettsinstituteoftechnology thehobsystemforverifyingsoftwaredesignproperties AT lampatrickphdmassachusettsinstituteoftechnology hobsystemforverifyingsoftwaredesignproperties |