所谓model checking，也就是自动验证系统的性质，比如有没有死锁，有没有starvation，有没有安全漏洞。这个方向的理论和实践都有重大进展。其中有意思的进展包括：
1. Amir Pnueli 1977年提出可以用时态逻辑形式化地验证系统设计，其中的突破是利用Kripke 59年提出的Kripke Structure描述系统，用Linear Temporal Logic描述系统性质。
2. Clarke 和 Emerson 80年带初提出用CTL （computational tree logic)来自动验证系统，并且给出了第一套验证的算法。不过那套算法的问题是不能解决状态爆炸问题。系统稍微大点，状态空间按指数级别组合，太耗费内存。但是，
3. Ken McMillan在1986年给出了用Ordered Binary Decision Diagram编码系统的方法，一下让验证算法可以处理上10亿状态，于是模型验证开始大规模进入工业界。
4. 虽然模型验证始终是NP-Hard的问题，但是还有其他方法，比如说mu-calculus, 各式有限状态的无穷自动机，abstract interpretation，还有利用SAT的验证。其中利用自动机的SPIN也有不错的工业应用。