Program analysis: are you a good developer?

After Rice’s theorem blew our mind, the world is willing to regain its feet and desperately makes up ways to shed some light on what's going on inside the programs. Data race detectors, model-checking, and other methods of dynamic analysis appear one after another. Meanwhile, static checkers, Javac plugins and other static analysis tools also start taking the stage. The mirage of automatic verification is looming large on the horizon. Our hero tries to make a quick review of these things, tries to use them in practice and eventually finds out that…