Skip to main content
SpringerLink
Log in

A Survey of High-Performance Computing for Software Verification

  • Conference paper
  • First Online:
Book cover Tools and Methods of Program Analysis (TMPA 2017)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 779))

Included in the following conference series:

Abstract

Automatic software verification is a high-demanded method for software quality assurance since it allows to prove the correctness of programs formally. However, any precise software verification technique requires a considerable amount of computational resources like memory and CPU time. Existing hardware architectures like multi-core CPUs distributed systems, clouds and GPUs can impressively boost verification performance. Developers of verification tools have to adapt their algorithms to modern hardware peculiarities for its productive employment. In the survey, we consider case studies of high-performance computing for speeding up and scaling verification of programs and program models.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Notes

  1. 1.

    Amazon Elastic Cloud EC2: http://aws.amazon.com/ec2.

  2. 2.

    Google App Engine: https://cloud.google.com/appengine/docs.

  3. 3.

    Why has CPU frequency ceased to grow: http://software.intel.com/en-us/blogs/2014/02/19/why-has-cpu-frequency-ceased-to-grow.

  4. 4.

    NVIDIA CUDA Computing Platform: http://nvidia.com/object/cuda_home_new.html.

References

  1. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  Google Scholar 

  2. Nori, A.V., Rajamani, S.K., Tetali, S.D., Thakur, A.V.: The Yogi project: software property checking via static analysis and testing. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 178–181. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_17

    Chapter  Google Scholar 

  3. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  4. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)

    Article  Google Scholar 

  5. Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)

    Google Scholar 

  6. Stern, U., Dill, D.L.: Parallelizing the Mur\({\varPhi }\) verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–267. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_26

    Chapter  Google Scholar 

  7. Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48234-2_3

    Chapter  Google Scholar 

  8. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st Symposium on Logic in Computer Science, pp. 332–344 (1986)

    Google Scholar 

  9. Barnat, J., Brim, L., Rockai, P.: Scalable shared memory LTL model checking. Int. J. Softw. Tools Technol. Transf. 12(2), 139–153 (2010)

    Article  Google Scholar 

  10. Rockai, P., Barnat, J., Lubos, B.: DiVinE 2.0: high-performance model checking. In: Proceedings of the 9th International Workshop on Parallel and Distributed Methods in Verification, Trento, pp. 31–32 (2009). https://doi.org/10.1109/HiBi.2009.10

  11. Barnat, J., Brim, L., Ročkai, P.: A time-optimal on-the-fly parallel algorithm for model checking of weak LTL properties. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 407–425. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10373-5_21

    Chapter  Google Scholar 

  12. Verstoep, K., Bal, H.E., Barnat, J., Brim, L.: Efficient large-scale model checking. In: 2009 IEEE International Symposium on Parallel Distributed Processing, pp. 1–12 (2009)

    Google Scholar 

  13. Message Passing Interface Forum: MPI: A Message-Passing Interface Standard Version 3.0 (2012). Chapter author for Collective Communication, Process Topologies, and One Sided Communications

    Google Scholar 

  14. Lopes, N.P., Rybalchenko, A.: Distributed and predictable software model checking. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 340–355. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_24

    Chapter  Google Scholar 

  15. Beyer, D.: Status report on software verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 373–388. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_25

    Chapter  Google Scholar 

  16. Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_55

    Chapter  Google Scholar 

  17. Beyer, D., Dresler, G., Wendler, P.: Software verification in the Google app-engine cloud. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 327–333. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_21

    Google Scholar 

  18. Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31759-0_19

    Chapter  Google Scholar 

  19. Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845–857 (2011)

    Article  Google Scholar 

  20. Holzmann, G.J.: Parallelizing the spin model checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 155–171. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31759-0_12

    Chapter  Google Scholar 

  21. 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). https://doi.org/10.1007/978-3-540-30494-4_25

    Chapter  Google Scholar 

  22. Brim, L., Černá, I., Moravec, P., Šimša, J.: How to order vertices for distributed LTL model-checking based on accepting predecessors. Electron. Notes Theor. Comput. Sci. 135(2), 3–18 (2006)

    Article  MATH  Google Scholar 

  23. Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model-checking. In: 18th IEEE International Conference on Automated Software Engineering, 2003 Proceedings, pp. 106–115 (2003)

    Google Scholar 

  24. Brim, L., Černá, I., Krčál, P., Pelánek, R.: Distributed LTL model checking based on negative cycle detection. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 96–107. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45294-X_9

    Chapter  Google Scholar 

  25. 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). https://doi.org/10.1007/978-3-642-20398-5_40

    Chapter  Google Scholar 

  26. Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, pp. 247–256. FMCAD Inc (2010)

    Google Scholar 

  27. Bošnački, D., Leue, S., Lafuente, A.L.: Partial-order reduction for general state exploring algorithms. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 271–287. Springer, Heidelberg (2006). https://doi.org/10.1007/11691617_16

    Chapter  Google Scholar 

  28. Laarman, A., van de Pol, J., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 38–56. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22306-8_4

    Chapter  Google Scholar 

  29. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

  30. Dalsgaard, A.E., Laarman, A., Larsen, K.G., Olesen, M.C., van de Pol, J.: Multi-core reachability for timed automata. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 91–106. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33365-1_8

    Chapter  Google Scholar 

  31. Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) Proceedings of the 14th International SPIN Workshop, Springer, Heidelberg, pp. 263–267 (2007)

    Google Scholar 

  32. Dean, J., Ghemawat, S.: Mapreduce: simplified data processing on large clusters. Commun. ACM 51(1), 107–113 (2008)

    Article  Google Scholar 

  33. Albarghouthi, A., Kumar, R., Nori, A.V., Rajamani, S.K.: Parallelizing top-down interprocedural analyses. SIGPLAN Not. 47(6), 217–228 (2012)

    Article  Google Scholar 

  34. Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: static driver verification with under 4. In: Proceedings of the 2010 International Conference Formal Methods in Computer Aided Design, pp. 35–42, October 2010

    Google Scholar 

  35. Barnat, J., Brim, L., Ceska, M., Lamr, T.: CUDA accelerated LTL model checking. In: Proceedings of the 15th International Conference on Parallel and Distributed Systems, pp. 34–41 (2009)

    Google Scholar 

  36. Barnat, J., Bauch, P., Brim, L., Ceska, M.: Employing multiple CUDA devices to accelerate LTL model checking. In: Proceedings of the 16th IEEE International Conference on Parallel and Distributed Systems, pp. 259–266 (2010)

    Google Scholar 

  37. Barnat, J., Bauch, P., Brim, L., EšKa, M.: Designing fast LTL model checking algorithms for many-core GPUs. J. Parallel Distrib. Comput. 72(9), 1083–1097 (2012)

    Article  Google Scholar 

  38. Bošnački, D., Edelkamp, S., Sulewski, D.: Efficient probabilistic model checking on general purpose graphics processors. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 32–49. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02652-2_7

    Chapter  Google Scholar 

  39. Burks, A.W., Warren, D.W., Wright, J.B.: An analysis of a logical machine using parenthesis-free notation. Math. Tables Other Aids Comput. 8(46), 53–57 (1954)

    Article  MathSciNet  MATH  Google Scholar 

  40. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

  41. Krylov, A.: On the numerical solution to the equation that defines frequencies of small oscilations of material systems in technical questions. Izv. Akad. Nauk SSSR Ser. Otdel. Mat. Estestv. Nauk 7(4), 491–539 (1931)

    Google Scholar 

  42. Bell, A., Haverkort, B.R.: Distributed disk-based algorithms for model checking very large markov chains. Form. Methods Syst. Des. 29(2), 177–196 (2006)

    Article  MATH  Google Scholar 

  43. Bartocci, E., DeFrancisco, R., Smolka, S.A.: Towards a GPGPU-parallel SPIN model checker. In: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014, pp. 87–96. ACM (2014)

    Google Scholar 

  44. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46029-2_13

    Chapter  Google Scholar 

  45. Bosnacki, D., Edelkamp, S., Sulewski, D., Wijs, A.: GPU-PRISM: an extension of prism for general purpose graphics processing units. In: Proceedings of the 2010 9th International Workshop on Parallel and Distributed Methods in Verification, PDMC-HIBI 2010, pp. 17–19. IEEE Computer Society (2010)

    Google Scholar 

  46. Wijs, A.J., Bošnački, D.: Improving GPU sparse matrix-vector multiplication for probabilistic model checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 98–116. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31759-0_9

    Chapter  Google Scholar 

  47. Wijs, A., Bošnački, D.: GPUexplore: many-core on-the-fly state space exploration using GPUs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 233–247. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_16

    Chapter  Google Scholar 

  48. Wijs, A., Neele, T., Bošnački, D.: GPUexplore 2.0: unleashing GPU explicit-state model checking. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 694–701. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_42

    Chapter  Google Scholar 

  49. Wijs, A., Bošnački, D.: Many-core on-the-fly model checking of safety properties using GPUs. Int. J. Softw. Tools Technol. Transf. 18(2), 169–185 (2016)

    Article  Google Scholar 

  50. Wijs, A.: BFS-based model checking of linear-time properties with an application on GPUs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 472–493. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_26

    Google Scholar 

  51. Neele, T., Wijs, A., Bošnački, D., van de Pol, J.: Partial-order reduction for GPU model checking. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 357–374. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_23

    Chapter  Google Scholar 

  52. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013)

    Article  MATH  Google Scholar 

  53. Prabhu, T., Ramalingam, S., Might, M., Hall, M.: EigenCFA: accelerating flow analysis with GPUs. SIGPLAN Not. 46(1), 511–522 (2011)

    Article  MATH  Google Scholar 

  54. Nori, A.V., Rajamani, S.K.: An empirical study of optimizations in YOGI. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, pp. 355–364 (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for System Programming of Russian Academy of Sciences, Moscow, Russia

    Ilja Zakharov

Authors
  1. Ilja Zakharov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ilja Zakharov .

Editor information

Editors and Affiliations

  1. St. Petersburg Polytechnic University, St. Petersburg, Russia

    Vladimir Itsykson

  2. University of Pennsylvania, Philadelphia, Pennsylvania, USA

    Andre Scedrov

  3. FRC CSC, Moscow, Russia

    Victor Zakharov

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zakharov, I. (2018). A Survey of High-Performance Computing for Software Verification. In: Itsykson, V., Scedrov, A., Zakharov, V. (eds) Tools and Methods of Program Analysis. TMPA 2017. Communications in Computer and Information Science, vol 779. Springer, Cham. https://doi.org/10.1007/978-3-319-71734-0_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71734-0_17

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation