Abstract.
Since its discovery in the early 1980s, model checking has emerged as one of the most exciting areas in the field of formal verification of system correctness. The chief reason for this enthusiasm resides in the fact that model checkers establish in a fully automated manner whether or not a system satisfies formal requirements; users need not construct proofs. Until the early 1990s, however, the practical impact of model checking was modest, in large part because the state-explosion problem limited the applicability of the technology. Recent advances in the field have dramatically expanded the scope of model checking, however, and interest in it on the part of practitioners is growing. This special section surveys several recent approaches to attacking the state explosion that are supporting the continued advancement of model checking as a viable technology for improved system design.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Cleaveland, R. Pragmatics of model checking: an STTT special section. STTT 2, 208–218 (1999). https://doi.org/10.1007/s100090050030
Issue Date:
DOI: https://doi.org/10.1007/s100090050030