{"id":{"repo_id":"vt","oai_identifier":"oai:vtechworks.lib.vt.edu:10919/81710"},"canonical_url":"https://search.dev.ndltd.org/etd/vt/oai:vtechworks.lib.vt.edu:10919/81710","repository":{"repo_id":"vt","name":"Virginia Tech","base_url":"https://vtechworks.lib.vt.edu/oai/request"},"display":{"title":"USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow","abstract":"Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software. This thesis presents USIMPL, a component of the Orca project for formal verification that builds on Foster’s Isabelle/UTP with features of Schirmer’s Simpl in order to achieve a modular, scalable framework for deductive proofs of program correctness utilizing Hoare logic and Hoare-style algebraic laws of programming.","abstract_html":"Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software. This thesis presents USIMPL, a component of the Orca project for formal verification that builds on Foster’s Isabelle/UTP with features of Schirmer’s Simpl in order to achieve a modular, scalable framework for deductive proofs of program correctness utilizing Hoare logic and Hoare-style algebraic laws of programming.","abstract_has_math":false,"creators":["Bockenek, Joshua A."],"institution":"Virginia Tech","degree_name":"Master of Science","degree_level":"masters","degree_discipline":"Computer Engineering","degree_department":"Electrical and Computer Engineering","school":null,"contributors":[],"advisors":[],"committee_chairs":["Ravindran, Binoy"],"committee_members":["Lammich, Peter","Broadwater, Robert P."],"year":2017,"date_issued":"2017-12-21","date_published":"2017-12-21","updated_at":"2026-07-22T22:19:39Z","subjects":["Formal Verification","Formal Methods","Isabelle","Unifying Theories of Programming","Verification Condition Generation"],"languages":["en_US"],"rights":["Creative Commons Attribution-ShareAlike 3.0 United States"],"rights_urls":["http://creativecommons.org/licenses/by-sa/3.0/us/"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10919/81710","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.committeechair","label":"Committee Chair","values":["Ravindran, Binoy"]},{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Lammich, Peter","Broadwater, Robert P."]},{"key":"dc:contributor.department","label":"Department","values":["Electrical and Computer Engineering"]},{"key":"dc:creator","label":"Author","values":["Bockenek, Joshua A."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2018-01-11T16:34:16Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2018-01-11T16:34:16Z"]},{"key":"dc:date.issued","label":"Date","values":["2017-12-21"]},{"key":"dc:publisher","label":"Institution","values":["Virginia Tech"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Virginia Polytechnic Institute and State University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Formal Verification","Formal Methods","Isabelle","Unifying Theories of Programming","Verification Condition Generation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en_US"]},{"key":"dc:rights","label":"Dc Rights","values":["Creative Commons Attribution-ShareAlike 3.0 United States"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://creativecommons.org/licenses/by-sa/3.0/us/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/10919/81710"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software. This thesis presents USIMPL, a component of the Orca project for formal verification that builds on Foster’s Isabelle/UTP with features of Schirmer’s Simpl in order to achieve a modular, scalable framework for deductive proofs of program correctness utilizing Hoare logic and Hoare-style algebraic laws of programming."]},{"key":"dc:description.abstractgeneral","label":"General Abstract","values":["Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software (OSes, compilers, and similar programs that have a high level of complexity but work on a lower level than typical user applications such as text editors, image viewers, and the like). This thesis presents USIMPL, a component of the Orca project for formal verification that builds on an existing framework for computer-aided, deductive mathematical proofs (Foster’s Isabelle/UTP) with features inspired by a simple but featureful language used for verification (Schirmer’s Simpl) in order to achieve a modular, scalable framework for proofs of program correctness utilizing the rule-based mathematical representation of program behavior known as Hoare logic and Hoare-style algebraic laws of programming, which provide a formal methodology for transforming programs to equivalent formulations."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Master of Science"]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["ETD"]},{"key":"dc:title","label":"Title","values":["USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow"]}]}],"canonical_facts":{"dc:contributor.committeechair":["Ravindran, Binoy"],"dc:contributor.committeemember":["Lammich, Peter","Broadwater, Robert P."],"dc:contributor.department":["Electrical and Computer Engineering"],"dc:creator":["Bockenek, Joshua A."],"dc:date.accessioned":["2018-01-11T16:34:16Z"],"dc:date.available":["2018-01-11T16:34:16Z"],"dc:date.issued":["2017-12-21"],"dc:description.abstract":["Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software. This thesis presents USIMPL, a component of the Orca project for formal verification that builds on Foster’s Isabelle/UTP with features of Schirmer’s Simpl in order to achieve a modular, scalable framework for deductive proofs of program correctness utilizing Hoare logic and Hoare-style algebraic laws of programming."],"dc:description.abstractgeneral":["Writing bug-free code is fraught with difficulty, and existing tools for the formal verification of programs do not scale well to large, complicated codebases such as that of systems software (OSes, compilers, and similar programs that have a high level of complexity but work on a lower level than typical user applications such as text editors, image viewers, and the like). This thesis presents USIMPL, a component of the Orca project for formal verification that builds on an existing framework for computer-aided, deductive mathematical proofs (Foster’s Isabelle/UTP) with features inspired by a simple but featureful language used for verification (Schirmer’s Simpl) in order to achieve a modular, scalable framework for proofs of program correctness utilizing the rule-based mathematical representation of program behavior known as Hoare logic and Hoare-style algebraic laws of programming, which provide a formal methodology for transforming programs to equivalent formulations."],"dc:description.degree":["Master of Science"],"dc:format.medium":["ETD"],"dc:identifier.uri":["http://hdl.handle.net/10919/81710"],"dc:language.iso":["en_US"],"dc:publisher":["Virginia Tech"],"dc:rights":["Creative Commons Attribution-ShareAlike 3.0 United States"],"dc:rights.uri":["http://creativecommons.org/licenses/by-sa/3.0/us/"],"dc:subject":["Formal Verification","Formal Methods","Isabelle","Unifying Theories of Programming","Verification Condition Generation"],"dc:title":["USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow"],"dc:type":["Thesis"],"thesis:degree_discipline":["Computer Engineering"],"thesis:degree_level":["masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["Virginia Polytechnic Institute and State University"]},"updated_at":"2026-07-22T22:19:39Z"}