Interference problems refer to the undesired interaction between aspects and base programs or interaction between aspects that results in unexpected functions and is harmful to the correctness of the entire program.The difficulty in detecting and fixing interferences in aspect-oriented designs impedes the widespread application of aspect-oriented programming paradigm.Suffered from the scalability problem, existing researches that use model checking techniques cannot effectively handle functional interferences.The paper designs and implements a tool that employs deduction-based technologies to support direct checking and remove functional interferences in aspect-oriented designs.This tool can automatically generate proof obligations excluding the existence of interference.In addition, the paper introduces the tool PVS to raise the automation level of verification.The proof can either ascertain no interference exists or give clues on how to rectify the design.