Statlig rymduppräkning
Inom datavetenskap är tillståndsrymduppräkning metoder som tar hänsyn till varje nåbart programtillstånd för att avgöra om ett program uppfyller en given egenskap. När program ökar i storlek och komplexitet tillståndsutrymmet exponentiellt. Tillståndsutrymmet som används av dessa metoder kan reduceras genom att endast behålla de delar av tillståndsutrymmet som är relevanta för analysen. Användningen av tillstånds- och minnesreduktionstekniker gör dock körtid till en stor begränsande faktor.