A comparison of modular verification techniques

Abstract

This paper presents and compares three techniques for mechanized verification of state-oriented design descriptions. The goat of this work is to gain insight into quantitative aspects of different modular verification techniques. One of the three verification techniques presented here is a traditional forward generationof a fixed point characterizing the reachable states. This does not utilize any modularity provided by the designer, and therefore it forms the basis for the comparison, whereas the two others do utilize such a modularity. One requires a substantial manual effort by the designer, but is computationally very efficient, while theother requires almost no manual assistance with a much better performance than the simple forward generation. The performance of the three techniques is compared on aset of examples.