Verifying Concurrent Systems