Reasoning and Verification: State of the Art and Current Trends
Bernhard Beckert and Reiner Hähnle
In this article, the authors give an overview of tool-based
verification of hardware and software systems and discuss the relation
between verification and logical reasoning. Here, "verification"
refers to reasoning-based methods to establish dependability. This
isn't restricted to proofs of functional correctness; it also includes
other scenarios such as test generation and bug finding. The authors
describe the main verification scenarios and methods that are in use
today and the extent to which they depend on logical reasoning. From
this discussion, they distill current trends and new opportunities for
the interaction between verification and reasoning.