Property-Driven Partitioning for Abstraction Refinement

Partitioning and abstraction have been studied extensively both in hardware and in software verification. The abstraction is typically partitioned according to the system design in the case of hardware or the control graph in the case of software. In this work we build on previous work on Property-Driven Partitioning (PDP), a hybrid Symbolic Model-Checking (SMC) technique for ω-regular properties in which the state space is partitioned according to the states of the property automaton. We investigate a new paradigm for abstraction refinement in SMC, which combines abstraction and PDP: each PDP partition may contain a different abstraction, so that it can be refined independently from the others; in case of a spurious counterexample π, the system is refined only in those partitions that are necessary to rule out π. We performed a preliminary experimental evaluation comparing standard Counterexample-Guided Abstraction Refinement (CEGAR) with its partitioned counterpart, which confirmed t...