Currently missing are: - Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts