Verifying real-world software with contracts for concurrency