Combining Static Analysis and Case-Based Search Space Partitioning for Reducing Peak Memory in Model Checking

Memory is one of the critical resources in model checking.This paper discusses a strategy for reducing peak memory in model checkingby case-based partitioning of the search space.This strategy combines model checking for verification of different cases andstatic analysis or expert judgment for guaranteeing the completeness ofthe cases. Description of the static analysis is basedon using PROMELA as the modeling language.The strategy is applicable to a subset of modelsincluding models for verification of certain aspects of protocols.