On Checking Model Checkers

Abstract

It has become good practice to expect authors of new model checking algorithms to provide not only rigorous evidence of the algorithms correctness, but also evidence of their practical significance. Though the rules for determining what is and what is not a good proof of correctness are clear, no comparable rules are usually enforced for determining the soundness of the data that is used to support the claim for practical significance. We consider here how we can flag the more common types of omission. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.