| Home > Publications > Reports > Informatics (CW) |
CW 549
Bart Jacobs, Frank Piessens
Dynamic Owicki-Gries reasoning using ghost fields and fractional permissions
Abstract
In this short note, we show how ghost fields and fractional permissions can be used to prove fork-join patterns. The approach is a simple port of Owicki and Gries's auxiliary variables-based approach to the setting with dynamic threads, locks, and objects.
report.pdf (145K) / mailto: B. Jacobs