{"id":{"repo_id":"byu","oai_identifier":"oai:scholarsarchive.byu.edu:etd-1190"},"canonical_url":"https://search.dev.ndltd.org/etd/byu/oai:scholarsarchive.byu.edu:etd-1190","repository":{"repo_id":"byu","name":"Brigham Young University","base_url":"https://scholarsarchive.byu.edu/do/oai/"},"display":{"title":"Disk Based Model Checking","abstract":"<p>Disk based model checking does not receive much attention in the model checking field becasue of its costly time overhead. In this thesis, we present a new disk based algorithm that can get close to or faster verification speed than a RAM based algorithm that has enough memory to complete its verification. This algorithm also outperforms Stern and Dill's original disk based algorithm. The algorithm partitions the state space to several files, and swaps files into and out of memory during verification. Compared with the RAM only algorithm, the new algoritm reduces hash table insertion time by reducing the cost and growth of the hash load. Compared with Stern's disk based algorithm, the new disk based algorithm significantly reduces disk vs memory comparsion but increases disk read/write time. The size of the model the new algorithm can verify is bound to the available disk size instead of the available RAM size.</p>","abstract_html":"<p>Disk based model checking does not receive much attention in the model checking field becasue of its costly time overhead. In this thesis, we present a new disk based algorithm that can get close to or faster verification speed than a RAM based algorithm that has enough memory to complete its verification. This algorithm also outperforms Stern and Dill's original disk based algorithm. The algorithm partitions the state space to several files, and swaps files into and out of memory during verification. Compared with the RAM only algorithm, the new algoritm reduces hash table insertion time by reducing the cost and growth of the hash load. Compared with Stern's disk based algorithm, the new disk based algorithm significantly reduces disk vs memory comparsion but increases disk read/write time. The size of the model the new algorithm can verify is bound to the available disk size instead of the available RAM size.</p>","abstract_has_math":false,"creators":["Bao, Tonglaga"],"institution":"Brigham Young University - Provo","degree_name":"MS","degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T01:27:25Z","subjects":["Model Checking","disk","Computer Sciences"],"languages":["English"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://scholarsarchive.byu.edu/etd/191","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Bao, Tonglaga"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2004-10-21T07:00:00Z"]},{"key":"dc:publisher","label":"Institution","values":["Brigham Young University - Provo"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["MS"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Model Checking","disk","Computer Sciences"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["English"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://scholarsarchive.byu.edu/etd/191","https://scholarsarchive.byu.edu/context/etd/article/1190/viewcontent/ETD_CISOPTR_210.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Physical and Mathematical Sciences; Computer Science"]},{"key":"dc:description.abstract","label":"Abstract","values":["<p>Disk based model checking does not receive much attention in the model checking field becasue of its costly time overhead. In this thesis, we present a new disk based algorithm that can get close to or faster verification speed than a RAM based algorithm that has enough memory to complete its verification. This algorithm also outperforms Stern and Dill's original disk based algorithm. The algorithm partitions the state space to several files, and swaps files into and out of memory during verification. Compared with the RAM only algorithm, the new algoritm reduces hash table insertion time by reducing the cost and growth of the hash load. Compared with Stern's disk based algorithm, the new disk based algorithm significantly reduces disk vs memory comparsion but increases disk read/write time. The size of the model the new algorithm can verify is bound to the available disk size instead of the available RAM size.</p>"]},{"key":"dc:format","label":"Dc Format","values":["application:pdf"]},{"key":"dc:source","label":"Dc Source","values":["Brigham Young University - Provo"]},{"key":"dc:title","label":"Title","values":["Disk Based Model Checking"]}]}],"canonical_facts":{"dc:creator":["Bao, Tonglaga"],"dc:date":["2004-10-21T07:00:00Z"],"dc:description":["Physical and Mathematical Sciences; Computer Science"],"dc:description.abstract":["<p>Disk based model checking does not receive much attention in the model checking field becasue of its costly time overhead. In this thesis, we present a new disk based algorithm that can get close to or faster verification speed than a RAM based algorithm that has enough memory to complete its verification. This algorithm also outperforms Stern and Dill's original disk based algorithm. The algorithm partitions the state space to several files, and swaps files into and out of memory during verification. Compared with the RAM only algorithm, the new algoritm reduces hash table insertion time by reducing the cost and growth of the hash load. Compared with Stern's disk based algorithm, the new disk based algorithm significantly reduces disk vs memory comparsion but increases disk read/write time. The size of the model the new algorithm can verify is bound to the available disk size instead of the available RAM size.</p>"],"dc:format":["application:pdf"],"dc:identifier":["https://scholarsarchive.byu.edu/etd/191","https://scholarsarchive.byu.edu/context/etd/article/1190/viewcontent/ETD_CISOPTR_210.pdf"],"dc:language":["English"],"dc:publisher":["Brigham Young University - Provo"],"dc:source":["Brigham Young University - Provo"],"dc:subject":["Model Checking","disk","Computer Sciences"],"dc:title":["Disk Based Model Checking"],"dc:type":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T01:27:25Z"}