A Hoare Logic Survey
- Supervisor Dr. Joseph Kiniry
- Subject Area Mathematics
- Pre-requisite Strong mathematical background and basic understanding of Hoare Logic
- Co-requisite (things you must learn along the way) Knowledge of PVS
- Subject Coverage Theoretical Computer Science
- Project Type Document the evolutionary history of Hoare Logic variants and compare and contrast the most popular and interesting variants
- Hardware/Software: Any machine running x86/Linux or Mac OS X
Description
Hoare Logic is a program logic introduced around thirty years ago that is used to reason about the correctness of programs with state. A large number of new logics have been developed over the years to handle new kinds of programming languages, concepts, and verification demands. For example, several groups performing program verification have recently chosen to use dynamic logic. The purpose of this project is to perform a survey of the evolution of Hoare Logic and gain a better understanding of some of the recently proposed related theories to understand if they are useful in an applied settings.
Mandatory
- Read the original Hoare logic paper.
- Read and discuss the Hoare logic survey book.
- Perform literature survey to map out evolutionary history of all modern Hoare logic variants
Discretionary
- Coauthor, submit, and publish a paper on this work.
- Attempt to encode one or more modern Hoare logics with respect to either our HOL object logic or our generic HOL semantics.
Sources of information and preparatory reading
- Hoare Logic entry in the Wikipedia
- Hoare Logic for Java in Isabelle/HOL
- The Bali project
- An axiomatic basis for computer programming, by C.A.R. Hoare
- Papers on Hoare Logic, particularly Lamport and Schneider's The "Hoare Logic" of CSP, and All That, Dynamic Logic by Harel et al, The 'Hoare Logic' of Concurrent Programs by Lamport, and Ten years of Hoare logic: A survey in ACM TOPLAS