ในวิทยาการคอมพิวเตอร์การแจงนับพื้นที่สถานะ เป็นวิธีการที่พิจารณา สถานะโปรแกรมที่เข้าถึงได้แต่ละสถานะเพื่อพิจารณาว่าโปรแกรมตรงตามคุณสมบัติที่กำหนดหรือไม่^{[ 1 ]}เมื่อโปรแกรมมีขนาดและความซับซ้อนเพิ่มขึ้นพื้นที่สถานะก็จะเพิ่มขึ้นแบบทวีคูณ พื้นที่สถานะที่ใช้โดยวิธีการเหล่านี้สามารถลดลงได้โดยการคงไว้เฉพาะส่วนของพื้นที่สถานะที่เกี่ยวข้องกับการวิเคราะห์เท่านั้น อย่างไรก็ตาม การใช้เทคนิคการลดสถานะและหน่วยความจำทำให้เวลารันไทม์เป็นปัจจัยจำกัดที่สำคัญ^{[ 2 ]}

• วิธีการที่เป็นทางการ
• การตรวจสอบแบบจำลอง