@inproceedings{ab66b3bc6e614418a8621a6a8171f82a,
title = "Tunneling and slicing: Towards scalable BMC",
abstract = "Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of lowlevel embedded industry programs.",
keywords = "BMC, CFG, CSR, EFSM, Partitioning, SMT, Slice, Tunnel",
author = "Malay Ganai and Aarti Gupta",
year = "2008",
doi = "10.1109/DAC.2008.4555797",
language = "English (US)",
isbn = "9781605581156",
series = "Proceedings - Design Automation Conference",
pages = "137--142",
booktitle = "Proceedings of the 45th Design Automation Conference, DAC",
note = "45th Design Automation Conference, DAC ; Conference date: 08-06-2008 Through 13-06-2008",
}