En informática , la enumeración de espacio de estado son métodos que consideran cada estado de programa alcanzable para determinar si un programa satisface una propiedad determinada. [1] A medida que los programas aumentan en tamaño y complejidad, el espacio de estado crece exponencialmente. El espacio de estado utilizado por estos métodos se puede reducir manteniendo solo las partes del espacio de estado que son relevantes para el análisis. Sin embargo, el uso de técnicas de reducción de estado y memoria hace que el tiempo de ejecución sea un factor limitante importante. [2]