Is there any reason why this work couldn't be done it parallel with kernel development?
There are parts of the kernel that are only touched rarely (ex. block/deadline-iosched, though there are probably better examples).
It seems as though this type of analysis might be good long term project.
Of course, if it is truly infeasible for any but the least interesting parts of the kernel then it is a waste of time.