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.

REFERENCES

• 1: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 2: A. Armando, J. Mantovani, and L. Platania. Bounded model checking of software using SMT solvers instead of SAT solvers. In Proc. of SPIN Workshop, 2006.
• 3: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 4: M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. V. Rossum, M. Schulz, and R. Sebastiani. The MathSAT 3 System. In Proc. of CADE, 2005.
• 5: R. Nieuwenhuis and A. Oliveras. DPLL(T) with exhaustive theory propogation and its application to difference logic. In Proc. of CAV, 2005.
• 6: B. Dutertre and L. de Moura. A fast linear-arithmetic solver for DPLL(T). In Proc. of CAV, 2006.
• 7: Malay K Ganai , Aarti Gupta, Accelerating high-level bounded model checking, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233664]
• 8: Malay Ganai , Aarti Gupta, SAT-Based Scalable Formal Verification Solutions (Series on Integrated Circuits and Systems), Springer-Verlag New York, Inc., Secaucus, NJ, 2007
• 9: Malay K. Ganai , Aarti Gupta , Zijiang Yang , Pranav Ashar, Efficient distributed SAT and SAT-based distributed Bounded Model Checking, International Journal on Software Tools for Technology Transfer (STTT), v.8 n.4, p.387-396, August 2006 [doi>10.1007/s10009-005-0203-z]
• 10: Malay K. Ganai , Aarti Gupta , Pranav Ashar, Beyond safety: customized SAT-based model checking, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065773]
• 11: Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
• 12: Tamir Heyman , Daniel Geist , Orna Grumberg , Assaf Schuster, Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits, Proceedings of the 12th International Conference on Computer Aided Verification, p.20-35, July 15-19, 2000
• 13: S. Barner and I. Rabinovitz. Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning. In Proceedings of CHARME, 2003.
• 14: Xiushan Feng , Alan J. Hu , Jin Yang, Partitioned model checking from software specifications, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China [doi>10.1145/1120725.1120967]
• 15: Chao Wang , Zijiang Yang , Franjo Ivančić , Aarti Gupta, Disjunctive image computation for embedded software verification, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
• 16: David Ward , Fabio Somenzi, Decomposing image computation for symbolic reachability analysis using control flow information, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233662]
• 17: S. Anand, C. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to java pathfinder. In Proc. of TACAS, pages 58--70, 2007.
• 18: T. Arons, E. Elster, S. Ozer, J. Shalev, and E. Singerman. Efficient symbolic simulation of low level software. In Proc. of DATE, 2008.
• 19: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 20: D. Babic and A. Hu. Structural abstraction of software verification conditions. In Proc. of CAV, 2007.
• 21: F. Ivančić, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-Soft: Software verification platform. In Proc. of CAV, 2005.
• 22: M. Dwyer and J. Hatcliff. Slicing software for model construction. In ACM Workshop on Partial Evaluation and Program Manipulation, 1999.
• 23: Radu Rugina , Martin Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.182-195, June 18-21, 2000, Vancouver, British Columbia, Canada
• 24: G. Karypis and V. Kumar. Multilevel k-way hypergraph partitioning. In Proc. Intl. Conf. on VLSI, 2000.
• 25: SRI. Yices: An SMT solver, http://fm.csl.sri.com/yices.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING

General Terms:
Algorithms, Experimentation, Performance, Verification

Keywords:
BMC, CFG, CSR, EFSM, SMT, partitioning, slice, tunnel