USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow
| dc.contributor.author | Bockenek, Joshua A. | en |
| dc.contributor.committeechair | Ravindran, Binoy | en |
| dc.contributor.committeemember | Lammich, Peter | en |
| dc.contributor.committeemember | Broadwater, Robert P. | en |
| dc.contributor.department | Electrical and Computer Engineering | en |
| dc.date.accessioned | 2018-01-11T16:34:16Z | en |
| dc.date.available | 2018-01-11T16:34:16Z | en |
| dc.date.issued | 2017-12-21 | en |
| 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. | en |
| 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. | en |
| dc.description.degree | Master of Science | en |
| dc.format.medium | ETD | en |
| dc.identifier.uri | http://hdl.handle.net/10919/81710 | en |
| dc.language.iso | en_US | en |
| dc.publisher | Virginia Tech | en |
| dc.rights | Creative Commons Attribution-ShareAlike 3.0 United States | en |
| dc.rights.uri | http://creativecommons.org/licenses/by-sa/3.0/us/ | en |
| dc.subject | Formal Verification | en |
| dc.subject | Formal Methods | en |
| dc.subject | Isabelle | en |
| dc.subject | Unifying Theories of Programming | en |
| dc.subject | Verification Condition Generation | en |
| dc.title | USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow | en |
| dc.type | Thesis | en |
| thesis.degree.discipline | Computer Engineering | en |
| thesis.degree.grantor | Virginia Polytechnic Institute and State University | en |
| thesis.degree.level | masters | en |
| thesis.degree.name | Master of Science | en |