A formula-driven modular attack on state explosion