MEMORY‐EFFICIENT STATE‐SPACE ANALYSIS IN SOFTWARE MODEL CHECKING
Zahir Tari, Péter Bertök, Anshuman Mukherjee · 2013
This chapter shows how the memory requirement for model checking could be reduced by storing states in difference form. Consequently, model checking would acquire a bigger role in the verification of a wide range of software. This ensures the safety and reliability of software systems and enhances their usability. Experimental results indicate that the models presented require significantly less memory to verify a software system. Furthermore, the solutions presented are found to perform better with larger models. Contemporary systems have a high level of complexity, often leading to large models. Therefore, the solutions presented are addressing a niche for such systems.