Techniques for managing state explosion and specialized algorithms for verifying classes of infinite state systems.