Abstraction refinement for state space partitioning based on auxiliary state machines

Counter-example guided abstraction refinement (CEGAR) techniques have been primarily used to scale the capacity of formal property verification. This paper explores the utility of CEGAR for verifying an emerging style of formal specifications, called AuxSM+properties, which consists of auxiliary state machines (AuxSMs) and formal properties based on the AuxSMs. A core challenge in formally verifying these specifications is in partitioning the states of the design-under-test (DUT) into sets which map into the different states of the AuxSM. In this paper we present a CEGAR approach for solving this problem without explicitly traversing the entire state space of the DUT.