Model Checking: Progress and Problems

摘要

Model checking is an automatic method of verifying finite state concurrent programs. The use of temporal logic and related frameworks to specify correctness has greatly facilitated simply thinking about the verification problem. Despite early worries about the intractability of state explosion, nowadays it can often be ameliorated, permitting verification of enormously large systems in practice. Important techniques include abstraction and compact (symbolic) representation.