Practical Aspects of Automated Deduction for Program Verification
Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rummer
Software is vital for modern society. It is used in many safety- or
security-critical applications, where a high degree of correctness is
desirable. Over the last years, technologies for the formal
specification and verification of software - using logic-based
specification languages and automated deduction - have matured and can
be expected to complement and partly replace traditional software
engineering methods in the future. Program verification is an
increasingly important application area for automated deduction. The
field has outgrown the area of academic case studies, and industry is
showing serious interest. This article describes the aspects of
automated deduction that are important for program verification in
practice, and it gives an overview of the reasoning mechanisms, the
methodology, and the architecture of modern program verification
systems.