Research in automating classical higher-order logic (HOL) has been on the rise for several years now and as a result, automated theorem provers for HOL, such as Satallax or LEO-II, are readily available. The area of application for these new tools is vast: The expressivity of the logic makes it easy to translate deduction problems of many facades into equialent problems in higher-order logic. This work is particularly concerned with solving problems in software verification, which can be addressed by, among others, the technique of model checking. In model checking, the state space of a program is insprected and exhaustively tested to whether it fulfils a certain property of interest or not. Such a property is commonly expressed in a verification logic, mostly temporal logics like LTL or CTL. We show how both the state space inspection and the verification logic can be embedded in HOL, and therefore how problems in model checking can be converted to problems for HOL theorem provers. The result is a verification software  which is not optimised for one specific verification logic, but can interpret program properties in an arbitrary logic, given an appropriate embedding in HOL. Furthermore, we present improvements for the current automated provers, which are required to treat such generated problems efficiently. These additions might also be highly relevant for problems in different domains and therefore thoroughly discussed.