At first sight the program verification is trustworthy and convenient, which is guaranteed by its well-developed formal basis. However, this method works smoothly in an ideal case only: a program and its annotations are correct, a domain theory is complete and a theorem prover is powerful enough. In case any of these prerequisites do not hold, the verification becomes much more complicated. Apart from possible defects in the foundations (which are not discussed here), one of the reasons is that verification, as a process, still relies on informal methods or implementation tricks. Error tracing is one of them. In this paper we would like to address this issue by giving a review of error localization and explanation methods developed in the C-light project. Their application is illustrated by examples.
