{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/81776"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/81776","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Efficient Explicit -State Model Checking for Programs With Dynamically Allocated Data","abstract":"We implemented Delta Execution in two model checkers, JPF (Java PathFinder) and BOX (Bounded Object eXploration) to evaluate the effectiveness of this technique in model checkers with different designs. The results show that DeltaExecution improves the overall exploration in both tools, but the improvements are due to different factors. We evaluate DeltaExecution on ten simple subject programs and a larger case study. The results show that DeltaExecution improves the exploration time for the smaller programs from 0.88x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX, while taking from 0.46x to 11.50x (with median 1.48x) less memory in JPF and from 0.18x to 2.71x (with median 1.18x) memory in BOX. The experimental results on one larger case study show that DeltaExecution improves the exploration time from 0.88x to 2.04x (with median 1.72x). Note that a ratio smaller than 1 means a slow down or use of more memory. Such ratios can arise in the exploration of small state-spaces.","abstract_html":"We implemented Delta Execution in two model checkers, JPF (Java PathFinder) and BOX (Bounded Object eXploration) to evaluate the effectiveness of this technique in model checkers with different designs. The results show that DeltaExecution improves the overall exploration in both tools, but the improvements are due to different factors. We evaluate DeltaExecution on ten simple subject programs and a larger case study. The results show that DeltaExecution improves the exploration time for the smaller programs from 0.88x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX, while taking from 0.46x to 11.50x (with median 1.48x) less memory in JPF and from 0.18x to 2.71x (with median 1.18x) memory in BOX. The experimental results on one larger case study show that DeltaExecution improves the exploration time from 0.88x to 2.04x (with median 1.72x). Note that a ratio smaller than 1 means a slow down or use of more memory. Such ratios can arise in the exploration of small state-spaces.","abstract_has_math":false,"creators":["d'Amorim, Marcelo"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Marinov, Darko"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015-09-25T20:20:24Z","date_published":"2015-09-25T20:20:24Z","updated_at":"2026-07-22T22:26:16Z","subjects":["Computer Science"],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["(MiAaPQ)AAI3290214"],"render_values":[{"text":"(MiAaPQ)AAI3290214","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/81776","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Marinov, Darko"]},{"key":"dc:creator","label":"Author","values":["d'Amorim, Marcelo"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2015-09-25T20:20:24Z","10000-01-01","2007"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/81776","(MiAaPQ)AAI3290214"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["We implemented Delta Execution in two model checkers, JPF (Java PathFinder) and BOX (Bounded Object eXploration) to evaluate the effectiveness of this technique in model checkers with different designs. The results show that DeltaExecution improves the overall exploration in both tools, but the improvements are due to different factors. We evaluate DeltaExecution on ten simple subject programs and a larger case study. The results show that DeltaExecution improves the exploration time for the smaller programs from 0.88x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX, while taking from 0.46x to 11.50x (with median 1.48x) less memory in JPF and from 0.18x to 2.71x (with median 1.18x) memory in BOX. The experimental results on one larger case study show that DeltaExecution improves the exploration time from 0.88x to 2.04x (with median 1.72x). Note that a ratio smaller than 1 means a slow down or use of more memory. Such ratios can arise in the exploration of small state-spaces.","Made available in DSpace on 2015-09-25T20:20:24Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 3290214.pdf: 3725896 bytes, checksum: 4c7a0995badafd72f651507b8e610bea (MD5) Previous issue date: 2007","Embargo set by: Seth Robbins for item 83057 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","121 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 2007."]},{"key":"dc:title","label":"Title","values":["Efficient Explicit -State Model Checking for Programs With Dynamically Allocated Data"]}]}],"canonical_facts":{"dc:contributor":["Marinov, Darko"],"dc:creator":["d'Amorim, Marcelo"],"dc:date":["2015-09-25T20:20:24Z","10000-01-01","2007"],"dc:description":["We implemented Delta Execution in two model checkers, JPF (Java PathFinder) and BOX (Bounded Object eXploration) to evaluate the effectiveness of this technique in model checkers with different designs. The results show that DeltaExecution improves the overall exploration in both tools, but the improvements are due to different factors. We evaluate DeltaExecution on ten simple subject programs and a larger case study. The results show that DeltaExecution improves the exploration time for the smaller programs from 0.88x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX, while taking from 0.46x to 11.50x (with median 1.48x) less memory in JPF and from 0.18x to 2.71x (with median 1.18x) memory in BOX. The experimental results on one larger case study show that DeltaExecution improves the exploration time from 0.88x to 2.04x (with median 1.72x). Note that a ratio smaller than 1 means a slow down or use of more memory. Such ratios can arise in the exploration of small state-spaces.","Made available in DSpace on 2015-09-25T20:20:24Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 3290214.pdf: 3725896 bytes, checksum: 4c7a0995badafd72f651507b8e610bea (MD5) Previous issue date: 2007","Embargo set by: Seth Robbins for item 83057 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","121 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 2007."],"dc:identifier":["http://hdl.handle.net/2142/81776","(MiAaPQ)AAI3290214"],"dc:language":["eng"],"dc:subject":["Computer Science"],"dc:title":["Efficient Explicit -State Model Checking for Programs With Dynamically Allocated Data"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:16Z"}