Towards Concurrent Hoare Logic

Type of content
Theses / Dissertations
Publisher's DOI/URI
Thesis discipline
Degree name
Other
Publisher
University of Canterbury
Journal Title
Journal ISSN
Volume Title
Language
English
Date
2012
Authors
Candy, Robin
Abstract

How can we rigorously prove that an algorithm does what we think it does? Logically verifying programs is very important to industry. Floyd-Hoare Logic (or Hoare Logic for short) is a set of rules that describe a type of valid reasoning for sequential program verification. Many different attempts have been made to extend Hoare Logic for concurrent program verification. We combine ideas from a few of these extensions to formalise a verification framework for specific classes of parallel programs. A new proof rule to deal with the semantics of mesh algorithms is proposed within the verification framework. We use the framework and mesh proof rule to verify the correctness of Sung Bae’s parallel algorithm for the maximum subarray problem.

Description
Citation
Keywords
Ngā upoko tukutuku/Māori subject headings
ANZSRC fields of research
Rights
All Right Reserved