Hardware and Software: Verification and Testing

Abstract

We present a tool d-TSR for parallelizing SMT-based BMC over a distributed environment targeted for checking safety properties in low-level embedded (sequential) software. We use a tunneling and slicing-based reduction (TSR) approach to decompose disjunctively a BMC instance (at a given depth) into simpler and independent subproblems. We exploit such a decomposition to cut down communication cost and idle time of CPUs during synchronization while solving BMC instances. Our approach scales almost linearly with number of CPUs, as demonstrated in our experimental results.