d-TSR: Parallelizing SMT-Based BMC Using Tunnels over a Distributed Framework | SpringerLink
Skip to main content
Springer Nature Link
Log in

d-TSR: Parallelizing SMT-Based BMC Using Tunnels over a Distributed Framework

  • Conference paper
Hardware and Software: Verification and Testing (HVC 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5394))

Included in the following conference series:

  • 399 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Ganai, M.K., Gupta, A., Yang, Z., Ashar, P.: Efficient distributed SAT and SAT-based distributed bounded model checking. Journal on STTT 8(4-5), 387–396 (2006)

    Article  MATH  Google Scholar 

  2. Abraham, E., Schubert, T., Becker, B., Franle, M., Herde, C.: Parallel sat solving in bounded model checking. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 301–315. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Barros, H., Campos, S., Song, M., Zarate, L.: Exploring clause symmetry in a distributed bounded model checking algorithm. In: ECBS (2007)

    Google Scholar 

  4. Jurkowiak, B., Li, C.M., Utard, G.: A parallelization scheme based on work stealing for a class of SAT solvers. Journal of Automatic Reasoning 34(1), 73–101 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  5. Blochinger, W., Sinz, C., Kuchlin, W.: Parallel propositional satifiability checking with distributed dynamic learning. Parallel Computing 29(7), 969–994 (2003)

    Article  Google Scholar 

  6. Ganai, M.K., Gupta, A.: Tunneling and Slicing: Towards Scalable BMC. In: Proc. of DAC (2008)

    Google Scholar 

  7. Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: Proc. of ICCAD (2006)

    Google Scholar 

  9. Burns, G., Daoud, R., Vaigl, J.: LAM: An Open Cluster Environment for MPI. In: Proceedings of Supercomputing Symposium, pp. 379–386 (1994)

    Google Scholar 

  10. Ganai, M.K., Gupta, A.: Completeness in SMT-based BMC for software programs. In: Proc. of DATE (2008)

    Google Scholar 

  11. SRI. Yices: An SMT solver, http://fm.csl.sri.com/yices

Download references

Author information

Authors and Affiliations

  1. NEC Labs America, Princeton, NJ, USA

    Malay K. Ganai & Weihong Li

Authors
  1. Malay K. Ganai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Weihong Li
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IBM Haifa Labs, Haifa University Campus, Mount Carmel, 31905, Haifa, Israel

    Hana Chockler

  2. Department of Computer Science, University of British Columbia, Vancouver, Canada

    Alan J. Hu

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ganai, M.K., Li, W. (2009). d-TSR: Parallelizing SMT-Based BMC Using Tunnels over a Distributed Framework. In: Chockler, H., Hu, A.J. (eds) Hardware and Software: Verification and Testing. HVC 2008. Lecture Notes in Computer Science, vol 5394. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01702-5_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-01702-5_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-01701-8

  • Online ISBN: 978-3-642-01702-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics