Jointly deployed aspects may interact with each other. While some interactions might be intended, unintended interactions (interferences) can break a program. Detecting and resolving interferences is particularly hard if aspects are developed independently, without knowledge of each other. Work on interference detection has focused so far on the correctness of weaved programs. In this paper we focus on the correctness and completeness of aspect weaving. We show that a large class of interferences result from incorrect or incomplete weaving and present a language independent correctness, completeness and non-interference analysis. Our technique can check aspect interferences independent of any base program and is applicable to aspects that contain implicit mutual dependencies in their implementation, without needing special purpose program annotations or formal specifications of aspect semantics. Categories and Subject Descriptors D.2.4 [Software Engineering]: Program Verification Ke...