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 Fosters...
Main Author: | |
---|---|
Other Authors: | , , , |
Format: | Thesis |
Language: | English |
Published: |
Virginia Tech
2017
|
Subjects: | |
Online Access: | http://hdl.handle.net/10919/81710 |
id |
ftvirginiatec:oai:vtechworks.lib.vt.edu:10919/81710 |
---|---|
record_format |
openpolar |
spelling |
ftvirginiatec:oai:vtechworks.lib.vt.edu:10919/81710 2024-05-19T07:46:47+00:00 USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow Bockenek, Joshua A. Electrical and Computer Engineering Ravindran, Binoy Lammich, Peter Broadwater, Robert P. 2017-12-21 ETD application/pdf http://hdl.handle.net/10919/81710 en_US eng Virginia Tech http://hdl.handle.net/10919/81710 Creative Commons Attribution-ShareAlike 3.0 United States http://creativecommons.org/licenses/by-sa/3.0/us/ Formal Verification Formal Methods Isabelle Unifying Theories of Programming Verification Condition Generation Thesis 2017 ftvirginiatec 2024-05-01T00:59:43Z 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 Fosters Isabelle/UTP with features of Schirmers 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. Master of Science 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 (Fosters Isabelle/UTP) with features inspired by a simple but featureful language used for verification (Schirmers 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. Thesis Orca VTechWorks (VirginiaTech) |
institution |
Open Polar |
collection |
VTechWorks (VirginiaTech) |
op_collection_id |
ftvirginiatec |
language |
English |
topic |
Formal Verification Formal Methods Isabelle Unifying Theories of Programming Verification Condition Generation |
spellingShingle |
Formal Verification Formal Methods Isabelle Unifying Theories of Programming Verification Condition Generation Bockenek, Joshua A. USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow |
topic_facet |
Formal Verification Formal Methods Isabelle Unifying Theories of Programming Verification Condition Generation |
description |
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 Fosters Isabelle/UTP with features of Schirmers 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. Master of Science 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 (Fosters Isabelle/UTP) with features inspired by a simple but featureful language used for verification (Schirmers 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. |
author2 |
Electrical and Computer Engineering Ravindran, Binoy Lammich, Peter Broadwater, Robert P. |
format |
Thesis |
author |
Bockenek, Joshua A. |
author_facet |
Bockenek, Joshua A. |
author_sort |
Bockenek, Joshua A. |
title |
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow |
title_short |
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow |
title_full |
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow |
title_fullStr |
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow |
title_full_unstemmed |
USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow |
title_sort |
usimpl: an extension of isabelle/utp with simpl-like control flow |
publisher |
Virginia Tech |
publishDate |
2017 |
url |
http://hdl.handle.net/10919/81710 |
genre |
Orca |
genre_facet |
Orca |
op_relation |
http://hdl.handle.net/10919/81710 |
op_rights |
Creative Commons Attribution-ShareAlike 3.0 United States http://creativecommons.org/licenses/by-sa/3.0/us/ |
_version_ |
1799487035700936704 |