Formal Verification of Concurrent Systems via Directed Model Checking