HONS 02/12
Towards Concurrent Hoare Logic
Robin Candy
Department of Computer Science and Software Engineering
University of Canterbury
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.
We combine ideas from a few of these extensions to formalize
a verification framework for specific classes of parallel programs.
A new proof rule to deal with the semantics of mesh algorithm 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.