  Bounded model checking (BMC) is a vital technique to find property violations
in programs. BMC can quickly find an execution path starting from an initial
state to the bad state that refutes a given property. However, BMC techniques
struggle to falsify programs that contain loops. BMC needs to unfold the
program loops up to the bound k, which sometimes leads to a considerable
state-space to be explored. Here, we develop an innovative software
verification approach that exploits interval methods via contractors to prune
the state-space exploration of programs that contain loops. In particular, this
is the first work that exploits interval methods via contractors to analyze the
loop variables search-space and identify where the property is guaranteed to
hold and prune the domain where it holds. Experimental results show a
performance boost in terms of space and time as contractors removed 99% of the
search-space in some examples and made them substantially faster to verify with
BMC.
