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

TR Number

Date

2017-12-21

Journal Title

Journal ISSN

Volume Title

Publisher

Virginia Tech

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.

Description

Keywords

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

Citation

Collections