USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow

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.

Name thesis:degree_name

Master of Science

Level thesis:degree_level

masters

Discipline thesis:degree_discipline

Computer Engineering

Department dc:contributor.department

Electrical and Computer Engineering

Grantor dc:publisher

Virginia Tech

Year dc:date.issued

2017

Author dc:creator

• Bockenek, Joshua A.

Chair dc:contributor.committeechair

• Ravindran, Binoy

Committee members dc:contributor.committeemember

• Lammich, Peter
• Broadwater, Robert P.

• Formal Verification
• Formal Methods
• Isabelle
• Unifying Theories of Programming
• Verification Condition Generation

Statement dc:rights

• Creative Commons Attribution-ShareAlike 3.0 United States

Licence dc:rights.uri

• http://creativecommons.org/licenses/by-sa/3.0/us/

Language dc:language.iso

en_US

Handle dc:identifier.uri

http://hdl.handle.net/10919/81710

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/81710