Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic

Hamed Nemati, Mads Dam

Shared-memory concurrency is notoriously difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments…