Model checking is an automatic verification technique for hardware and software systems that are finite state or have finite state abstractions. It has been used successfully to verify computer hardware, and it is beginning to be used to verify computer software as well.
As the number of state variables in the system increases, the size of the system state space grows exponentially. This is called the "state explosion problem". Much of the research in model checking over the past 30 years has involved developing techniques for dealing with this problem.