MEMORY-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODEL CHECKING
Formal methods have an unprecedented ability to endorse the correctness of a system. Despite that, they have been limited to safety- and mission-critical systems, owing to the significant time and memory costs involved. Our ever-increasing dependency on software in many aspects of life has necessitated the use of formal methods for a wider range of software. In this chapter we present two techniques to reduce the memory requirement of model checking, a widely used formal method. To ensure termination a model checker stores in memory all states explored. The techniques presented slash memory costs by storing a state according to how different it is from one of its neighboring states. Our experiments report a memory reduction of 95% while only doubling the computation delay. This reduction allows model checking in a machine with only a fraction of the memory required otherwise. Consequently, the advantage is twofold: (1) the savings substantial are, as a smaller physical memory suffices; and (2) as more states can now be stored in a memory of the same size, the chances of accomplishing complete state-space analysis are considerably higher.
Traditionally, software is considered “fail-safe” if it has passed a rigorous testing phase . However, the crash of the Ariane 5 launcher  and the deaths due to malfunctioning of the Therac-25 radiation therapy machine , despite rigorous software ...