USIMPL: An Extension of Isabelle/UTP with Simpl-like Control Flow
Files
TR Number
Date
2017-12-21
Authors
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