Software Verification and Scientific Methodology: Models, Regularities, Idealizations

Essential traits of model checking, a prominent formal method utilized in computer science to predict future behaviours of software systems, are examined here in the framework of the model-based paradigm of scientific reasoning. Models that model checking techniques enable one to develop are shown to satisfy logical re-quirements expressed by the set-theoretic view of scientific models. It is highlighted how model checking algorithms are able to isolate law-like generalizations holding in the model under given ceteris paribus conditions and concerning software executions. Further-more, abstraction methodologies utilized in model checking to de-crease the state space of complex models are taken to be instantia-tions of the general process known as Aristotelian abstraction char-acterizing empirical modelling. Finally, the methodological interest of the model-checking techniques is emphasized in connection with the debate concerning the epistemological status of computer sci-ence.