We explore the effectiveness of abstract interpretation in detecting parts of program specifications that can be simplified statically to true or false, as well as the impact of such analysis in reducing the cost of the run-time checks required for the remaining parts of these specifications.

Based on an operational semantics for programs with assertion checking, and the results of abstract interpretation, we recall the corresponding analysis-based assertion simplification problem, and propose and study a number of practical assertion checking modes, each of which represents a trade-off between code annotation depth, execution time slowdown, and program behavior safety.

We propose techniques for taking advantage of the run-time checking semantics to improve the precision of the analysis. We also report on some experimental results on the effectiveness of the techniques proposed.