RGSep is a program logic that combines rely-guarantee reasoning and separation logic. It has been used, both manually and automatically, to prove the correctness of several fine-grained concurrent algorithms.

Material

Tool support

Related program logics

Imprint | Data protection