Through a novel combination of both forward technique to compute contextual 
constraint, and backward method to derive weakest pre-conditions, ABCE 
algorithm represents a comprehensive method for handling both totally 
redundant and partially redundant checks. Translation from imperative code to 
SSA form is done in the same phase as the forward analysis, and the code that 
is added (substitutions, and conversion from while loop) is not significant in 
size. 

Our implementation needs currently annotations in order to handle loops and 
inter- procedural propagation. We also describe a fix-point computation that 
could be used to infer the loop invariants and function’s sized type. Our 
prototype analyzer works on a small subset of an imperative language, which we 
plan to extend further.