The following technical report is available from http://aib.informatik.rwth-aachen.de: Automatic Verification of the Correctness of the Upper Bound of a Maximum Independent Set Algorithm Felix Reidl, Fernando Sánchez Villaamil AIB 2009-10 Kneis, Langer and Rossmanith presented a new exact algorithm for the Maximum Independent Set problem. As part of the proof of the upper runtime bound millions of special cases were automatically generated. In this technical report we present a verification method that checks the correctness of this case distinction. We focus on the theoretical aspects of this verification and give a general overview of its implementation.