{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/53102"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/53102","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Runtime verification of object lifetime specifications","abstract":"This thesis reports on the implementation of a runtime verification system for object lifetime specifications. This system is used to explore and evaluate the expressiveness object lifetime specifications. Object lifetime specifications are program annotations that indicate, in terms of program execution, when objects should be reclaimed. Object lifetime specifications are designed to be used within the context of an object-oriented programming language with automatic storage reclamation (i.e., garbage collection). Our runtime verification system observes program execution and reports objects that are not re-claimed before the end of their specified lifetime. We implement our system with the Java Path Finder model-checking framework. JPF supports modeling non-determinism in programs. We leverage this support to verify all possible thread interleavings when checking user programs.","abstract_html":"This thesis reports on the implementation of a runtime verification system for object lifetime specifications. This system is used to explore and evaluate the expressiveness object lifetime specifications. Object lifetime specifications are program annotations that indicate, in terms of program execution, when objects should be reclaimed. Object lifetime specifications are designed to be used within the context of an object-oriented programming language with automatic storage reclamation (i.e., garbage collection). Our runtime verification system observes program execution and reports objects that are not re-claimed before the end of their specified lifetime. We implement our system with the Java Path Finder model-checking framework. JPF supports modeling non-determinism in programs. We leverage this support to verify all possible thread interleavings when checking user programs.","abstract_has_math":false,"creators":["Benjamin, Zev (Zev A.)"],"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 Jackson."],"committee_chairs":[],"committee_members":[],"year":2009,"date_issued":"2009","date_published":"2009","updated_at":"2026-07-22T22:21:34Z","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/53102","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Daniel 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":["Benjamin, Zev (Zev A.)"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2010-03-25T15:01:16Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2010-03-25T15:01:16Z"]},{"key":"dc:date.issued","label":"Date","values":["2009"]},{"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/53102"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2009.","Includes bibliographical references (leaves 48-49)."]},{"key":"dc:description.abstract","label":"Abstract","values":["This thesis reports on the implementation of a runtime verification system for object lifetime specifications. This system is used to explore and evaluate the expressiveness object lifetime specifications. Object lifetime specifications are program annotations that indicate, in terms of program execution, when objects should be reclaimed. Object lifetime specifications are designed to be used within the context of an object-oriented programming language with automatic storage reclamation (i.e., garbage collection). Our runtime verification system observes program execution and reports objects that are not re-claimed before the end of their specified lifetime. We implement our system with the Java Path Finder model-checking framework. JPF supports modeling non-determinism in programs. We leverage this support to verify all possible thread interleavings when checking user programs."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M.Eng."]},{"key":"dc:title","label":"Title","values":["Runtime verification of object lifetime specifications"]}]}],"canonical_facts":{"dc:contributor.advisor":["Daniel 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":["Benjamin, Zev (Zev A.)"],"dc:date.accessioned":["2010-03-25T15:01:16Z"],"dc:date.available":["2010-03-25T15:01:16Z"],"dc:date.issued":["2009"],"dc:description":["Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2009.","Includes bibliographical references (leaves 48-49)."],"dc:description.abstract":["This thesis reports on the implementation of a runtime verification system for object lifetime specifications. This system is used to explore and evaluate the expressiveness object lifetime specifications. Object lifetime specifications are program annotations that indicate, in terms of program execution, when objects should be reclaimed. Object lifetime specifications are designed to be used within the context of an object-oriented programming language with automatic storage reclamation (i.e., garbage collection). Our runtime verification system observes program execution and reports objects that are not re-claimed before the end of their specified lifetime. We implement our system with the Java Path Finder model-checking framework. JPF supports modeling non-determinism in programs. We leverage this support to verify all possible thread interleavings when checking user programs."],"dc:description.degree":["M.Eng."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/53102"],"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":["Runtime verification of object lifetime specifications"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:21:34Z"}