Towards Concurrent Hoare Logic

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