Bounded Model Checking of Software Using Interval Methods via Contractors

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.