The use of formal methods has been growing steadily and there have been a number of successful applications of formal methods in a range of application areas. It seems agreed that quality should be assured by applying testing, analysis and formal methods to rigorously de ned precode artifacts. The detection of null pointer violation errors is de nitely such a goal. This way of applying formal methods has a great potential to increase our con dence in the software. Our goal is to provide a practical mechanism to assist the application of formal methods in the early detection of null pointer violation errors in programs. Our solution is theorem proving based and is focused on the identi cation of the possible places in which a theorem prover could assist in the detection of null pointer violation errors and the formulation of the necessary proof obligations.