Model Checking: Software and Beyond

Edmund Clarke; Flavio Lerda

doi:10.3217/jucs-013-05-0639

JUCS - Journal of Universal Computer Science 13(5): 639-649, doi: 10.3217/jucs-013-05-0639

Model Checking: Software and Beyond

Edmund M. Clarke^‡, Flavio Lerda^‡

‡ Carnegie Mellon University, Pittsburgh, United States of America

Corresponding author: Edmund Clarke ( emc@cs.cmu.edu )

This article is freely available under the J.UCS Open Content License.

Citation: Clarke EM, Lerda F (2007) Model Checking: Software and Beyond. JUCS - Journal of Universal Computer Science 13(5): 639-649. https://doi.org/10.3217/jucs-013-05-0639

Abstract

This paper introduces model checking, originally conceived for checking finite statesystems. It surveys its evolution to encompass finitely checkable properties of systems with unbounded state spaces, and its application to software and other systems.

Keywords

formal methods, model checking