Dead-Code Detection with IC3 using SMT-LIBv2 Solvers

Abstract:
In this case study we evaluate an SMT-based IC3 implementation which is designed for formally proving the absence of dead-code in embedded C code. Our IC3 implementation is able to use any off-the-shelf SMT-LIBv2 solver which allows solving under assumptions and supports QF_BVFP.We extend the basic IC3 generalization techniques by splitting theory variables into intervals enabling more fine grained reasoning. We compare different state-of-the-art SMT-LIBv2 solvers and evaluate how their performance is affected by optimizations of IC3, like target enlargement or stronger generalization of proof obligations, as well as a preprocessing technique known as constant elimination that has proven to be very effective in our application context. We further evaluate how IC3 with SMT-LIBv2 solvers and interval-based generalization competes in comparison to iSAT3+IC3 as a part of BTC EmbeddedPlatform(r) which we currently consider the strongest stand-alone engine in dead-code detection on floating-point dominated benchmarks.