Abstract for HONS 02/12 - Computer Science and Software Engineering - University of Canterbury - New Zealand
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.
  • Phone: +64 3 369 2777
    Fax: +64 3 364 2569
    CSSEadministration@canterbury.ac.nz
  • Computer Science and Software Engineering
    University of Canterbury
    Private Bag 4800, Christchurch
    New Zealand
  • Follow us
    FacebookYoutubetwitterLinked In