  This essay is divided in four parts: In section (I) I explain why I think
detecting hot-spots in verification is complicated and in particular, more
complicated than detection when developing crude software. In section (II) I
introduce the factors I think mostly affect performance in verification. In
section (III) I propose a method to find functions that are most promising to
be optimized. Finally, in section (IV) I draw some conclusions and discuss
pros/cons of the proposed solution.
