Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling

Abstract

In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in previous years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced and-inverter graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well