Automated Deduction - A Basis for Applications Wolfgang Ahrendt, Bernhard Beckert, Reiner Haehnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, Peter H. Schmitt Integrating Automated and Interactive Theorem Proving This chapter highlights a project to integrate interactive and automated theorem proving in software verification. Its aim is to combine the advantages of the two paradigms. We report on the integration concepts and on the experimental results with a prototype implementation.