Show simple item record

dc.contributor.authorBockenek, Joshua A.en_US
dc.date.accessioned2018-01-11T16:34:16Z
dc.date.available2018-01-11T16:34:16Z
dc.date.issued2017-12-21en_US
dc.identifier.urihttp://hdl.handle.net/10919/81710
dc.description.abstractWriting 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.en_US
dc.format.mediumETDen_US
dc.language.isoen_USen_US
dc.publisherVirginia Techen_US
dc.rightsAttribution-ShareAlike 3.0 United States*
dc.rights.urihttp://creativecommons.org/licenses/by-sa/3.0/us/*
dc.subjectFormal Verificationen_US
dc.subjectFormal Methodsen_US
dc.subjectIsabelleen_US
dc.subjectUnifying Theories of Programmingen_US
dc.subjectVerification Condition Generationen_US
dc.titleUSIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flowen_US
dc.typeThesisen_US
dc.contributor.departmentElectrical and Computer Engineeringen_US
dc.description.degreeMaster of Scienceen_US
thesis.degree.nameMaster of Scienceen_US
thesis.degree.levelmastersen_US
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen_US
thesis.degree.disciplineComputer Engineeringen_US
dc.contributor.committeechairRavindran, Binoyen_US
dc.contributor.committeememberLammich, Peteren_US
dc.contributor.committeememberBroadwater, Robert P.en_US
dc.description.abstractgeneralWriting 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.en_US


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution-ShareAlike 3.0 United States
License: Attribution-ShareAlike 3.0 United States