Verification of the HARPO language

Abstract

Verification of sequential programs is hard. Verification of concurrent programs is even harder because it involves considering the possibility of thread interference in addition to the complexity of sequential reasoning. The purpose of this thesis is to develop a methodology for the automated verification of the multi-threaded and object-oriented HARPO/L language. A verification methodology is presented which allows verifying a program based on its contracts. In particular, it gaurantees data-race-freedom, verification of data invariants (i.e. ab- sence of data corruption), and, to the extent that the pre- and postconditions specify it, correctness of the interface to shared objects. The methodology is built based on implicit dynamic frames with fractional permissions. A specification language is developed based on this methodology to allow programmers to express their de- sign decisions formally. The verification technique is based on verification-condition generation and automated theorem proving. A translation from HARPO/L to the intermediate verification language, Boogie, is provided in the thesis. The e¢ cacy of this approach is demonstrated by translating several examples to Boogie and using automated verification on the translation.