Owicki--Gries Logic for Timestamp Semantics

Tatsuya Abe

Whereas an extension with non-interference of Hoare logic for sequential programs Owicki--Gries logic ensures the correctness of concurrent programs on strict consistency, it is un…