Model checking multithreaded programs by means of reduced models