{"id":{"repo_id":"byu","oai_identifier":"oai:scholarsarchive.byu.edu:etd-2385"},"canonical_url":"https://search.dev.ndltd.org/etd/byu/oai:scholarsarchive.byu.edu:etd-2385","repository":{"repo_id":"byu","name":"Brigham Young University","base_url":"https://scholarsarchive.byu.edu/do/oai/"},"display":{"title":"Machine Code Verification Using The Bogor Framework","abstract":"Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an \"off-the-shelf\" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features such as instruction execution, exceptional control flow, and interrupt servicing as extensions to Bogor. These extensions work within the tool framework using existing interfaces and require significantly less code than creating an entire model checking tool.","abstract_html":"Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an "off-the-shelf" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features such as instruction execution, exceptional control flow, and interrupt servicing as extensions to Bogor. These extensions work within the tool framework using existing interfaces and require significantly less code than creating an entire model checking tool.","abstract_has_math":false,"creators":["Edelman, Joseph R."],"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:29:12Z","subjects":["Bogor","model checking","language extension","embedded systems verification","Computer Sciences"],"languages":["English"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://scholarsarchive.byu.edu/etd/1386","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Edelman, Joseph R."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2008-05-22T07: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":["Bogor","model checking","language extension","embedded systems verification","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/1386","https://scholarsarchive.byu.edu/context/etd/article/2385/viewcontent/ETD_CISOPTR_1390.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":["Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an \"off-the-shelf\" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features such as instruction execution, exceptional control flow, and interrupt servicing as extensions to Bogor. These extensions work within the tool framework using existing interfaces and require significantly less code than creating an entire model checking tool."]},{"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":["Machine Code Verification Using The Bogor Framework"]}]}],"canonical_facts":{"dc:creator":["Edelman, Joseph R."],"dc:date":["2008-05-22T07:00:00Z"],"dc:description":["Physical and Mathematical Sciences; Computer Science"],"dc:description.abstract":["Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an \"off-the-shelf\" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features such as instruction execution, exceptional control flow, and interrupt servicing as extensions to Bogor. These extensions work within the tool framework using existing interfaces and require significantly less code than creating an entire model checking tool."],"dc:format":["application:pdf"],"dc:identifier":["https://scholarsarchive.byu.edu/etd/1386","https://scholarsarchive.byu.edu/context/etd/article/2385/viewcontent/ETD_CISOPTR_1390.pdf"],"dc:language":["English"],"dc:publisher":["Brigham Young University - Provo"],"dc:source":["Brigham Young University - Provo"],"dc:subject":["Bogor","model checking","language extension","embedded systems verification","Computer Sciences"],"dc:title":["Machine Code Verification Using The Bogor Framework"],"dc:type":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T01:29:12Z"}