A Concurrent Program Logic with a Future and History

Roland Meyer, Thomas Wies, Sebastian Wolff

Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal w…