Visible to the public Verified Compiler Technology and Separation Logic for Reasoning about Concurrent C Programs