: This paper introduces model checking, originally conceived for checking finite state systems. It surveys its evolution to encompass finitely checkable properties of systems with unbounded state spaces, and its application to software and other systems. Key Words: Formal Methods, Model Checking Category: D.2.4, F.3.1, B.2
Edmund M. Clarke, Flavio Lerda