Verifying Concurrent Programs by Memory Unwinding