Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization