Generating Rely-Guarantee Conditions with the Conditional-Writes Domain

James Tobler, Graeme Smith

Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, i…