Verifying Real-World Software with Contracts for Concurrency