Skip to main content
SpringerLink
Log in

Context-Switch-Directed Verification in DIVINE

  • Conference paper
  • First Online:
Book cover Mathematical and Engineering Methods in Computer Science (MEMICS 2014)

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

Abstract

In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed exploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs.

P. Ročkai—The contribution of Petr Ročkai has been partially supported by Red Hat, Inc.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 34.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 1–15. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 107–123. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Barnat, J., et al.: DiVinE 3.0 – An explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863–868. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Barnat, J., Brim, L., Ročkai, P.: On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming 77(12), 1272–1288 (2012)

    Article  MATH  Google Scholar 

  5. Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 207–220. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Brim, L., Černá, I., Moravec, P., Šimša, J.: Accepting predecessors are better than back edges in distributed LTL model-checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 352–366. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)

    Google Scholar 

  8. Godefroid, P.: Model checking for programming languages using verisoft. In: POPL, pp. 174–186. ACM Press (1997)

    Google Scholar 

  9. Holzmann, G.J.: The Spin Model Checker Primer and Reference Manual. Addison-Wesley (2004)

    Google Scholar 

  10. Holzmann, G.J., Florian, M.: Model checking with bounded context switching. Formal Aspects of Computing 23(3), 365–389 (2011)

    Article  MATH  Google Scholar 

  11. Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Transactions on Software Engineering 37(6), 845–857 (2011)

    Article  Google Scholar 

  12. Laarman, A., van de Pol, J., Weber, M.: Multi-Core LTSmin: marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506–511. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: ACM SIGPLAN, PLDI, PLDI 2007, pp. 446–455. ACM, New York (2007)

    Google Scholar 

  14. Musuvathi, M., Qadeer, S.: Partial-Order Reduction for Context-Bounded State Exploration. Technical Report MSR-TR-2007-12, Microsoft Research (2007)

    Google Scholar 

  15. Musuvathi, M., Qadeer, S.: Fair Stateless Model Checking. ACM SIGPLAN Notices 43(6), 362–371 (2008)

    Article  Google Scholar 

  16. Nagarakatte, S., Burckhardt, S., Martin, M.M.K., Musuvathi, M.: Multicore acceleration of priority-based schedulers for concurrency bug detection. In: ACM SIGPLAN, PLDI, pp. 543–554. ACM (2012)

    Google Scholar 

  17. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, Lenore D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Ročkai, P., Barnat, J., Brim, L.: Improved state space reductions for LTL model checking of C and C++ programs. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 1–15. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Informatics, Masaryk University, Brno, Czech Republic

    Vladimír Štill, Petr Ročkai & Jiří Barnat

Authors
  1. Vladimír Štill
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Petr Ročkai
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jiří Barnat
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vladimír Štill .

Editor information

Editors and Affiliations

  1. Masaryk University, Brno, Czech Republic

    Petr Hliněný

  2. Charles University, Praha, Czech Republic

    Zdeněk Dvořák

  3. Brno University of Technology, Brno, Czech Republic

    Jiří Jaroš

  4. Charles University, Praha, Czech Republic

    Jan Kofroň

  5. Brno University of Technology, Brno, Czech Republic

    Jan Kořenek

  6. Masaryk University, Brno, Czech Republic

    Petr Matula

  7. Masaryk University, Brno, Czech Republic

    Karel Pala

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Štill, V., Ročkai, P., Barnat, J. (2014). Context-Switch-Directed Verification in DIVINE. In: Hliněný, P., et al. Mathematical and Engineering Methods in Computer Science. MEMICS 2014. Lecture Notes in Computer Science(), vol 8934. Springer, Cham. https://doi.org/10.1007/978-3-319-14896-0_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-14896-0_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-14895-3

  • Online ISBN: 978-3-319-14896-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation