Students in the second introductory programming course at Carnegie Mellon routinely have trouble learning how to properly use pointers. The course is taught in C0, a simple, safe C-subset. A common error in student's code is to dereference a pointer which may be NULL. The goal of this thesis is to evaluate whether automated program analysis can provide useful feedback to students. Typically program analysis is difficult even for experts to operate, because the analysis must consider the whole program at once. Instead of these approaches, we use student supplied specifications, such as pre- and post-conditions, to guide the analysis. We developed a tool which analyzes a program and determines whether each dereference in a program is guaranteed to be safe, will definitely cause a crash, or is unknown. We ran our tool on a corpus of student homework submissions from several semesters of the introductory programming course, and evaluated a random subset of the errors to determine whether they were accurate. We determined that on simple assignments, a large fraction of the errors were accurate, but that on more complicated assignments with complex invariants, the rate of incorrect errors was much higher. Future extensions of this work would compare student learning with and without the tool, as well as investigate ways to improve accuracy on the more involved assignments.