Verification of concurrent HARPO programs using formal verification theory

Abstract

Defects in software cost money and sometimes lives. Even with rigorous testing, there are countless ways for programs to go wrong. Testing does not guarantee that a given program is correct for every input. Concurrent program testing does not guarantee that a program is correct for the example inputs. Formal program verification has been used as a technique to ensure program correctness for several years. It analyses the properties of the code and ensures that nothing goes wrong. In this thesis, a formal verification tool is designed and implemented based on Boogie IVL (Intermediate Verification Language) for a multi-threaded and object-oriented language named HARPO (HARdware Parallel Objects). We have designed the specific annotations intended only for use in verification. These annotations help the HARPO verifier to translate the program into an equivalent Boogie code. The resulting Boogie code is checked with theorem provers to verify the correctness of the HARPO program. Boogie code generation is tested using unit testing, and some of the case studies are reported. Consequently, programmers can use the HARPO verifier for verification of their concurrent programs.