Keywords: Concurrency; structural operational semantics; verification Units: 12/24 units
Description: In Hoare logic, relative completeness refers to the property that the proof system is complete relative to the underlying logic of assertions. Formally, it means that if a Hoare triple {P} C {Q} is semantically valid (if every terminating execution of program C starting in a state satisfying P ends in a state satisfying Q) then there exists a formal proof of this triple provided all necessary facts about the underlying expressions and predicates can be established. In other words, Hoare logic can prove every true partial correctness assertion, assuming one can reason perfectly about the mathematical assertions used within it.
When considering concurrent systems, Hoare Logic is usually be replaced by techniques developed by Owicki/Griess and Jones, respectively. It is well established that the Owicki-Griess method is relative complete as well, assuming one allows ghost variables. The situation is different for Jones’ Rely-Guarantee (RG).
There exists a complicated proof stating that the RG method is relative complete, relative to an underlying trace model. At the same time, Jones himself strongly believes that the methodology is incomplete.
The goal of the project is a careful investigation into the (relative) completeness of the RG-method