Model Checking Large Design Space: Theory, Tools, and Experiments

Abstract

This dissertation studies how to scale model checking across large design spaces rather than isolated models. It develops theory, algorithms, and experimental techniques for design-space reduction, incremental verification, multi-property verification, and parallel orchestration, showing how relationships among models and properties can be exploited to improve verification efficiency without sacrificing coverage.