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.