C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs | SpringerLink
Skip to main content
Springer Nature Link
Log in

C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2021)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12864))

Included in the following conference series:

Abstract

Finding programming errors is one of the major challenges in software development. Formal methods such as model checking have become a popular approach to address this problem because of their guarantees about error status. However, one of the greatest challenges is to have correct information about complex internal details such as memory, registers, and system state. In this paper we describe the C-SMC tool and methodology developed to find programming errors in C programs by leveraging statistical model checking and runtime information. Our prototype shows that our approach can complement many existing software verification tools.

This work has been partially supported by a Cisco grant.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

References

  1. Coverity Scan. https://scan.coverity.com/. Accessed 18 Jan 2021

  2. CPPCheck: A tool for static C/C++ code analysis. http://cppcheck.sourceforge.net/. Accessed 18 Jan 2021

  3. Debugging Dynamic Memory Usage Errors Using HP WDB. http://www.3kranger.com/HP3000/mpeix/en-hpux/PDF/5014-0301.pdf. Accessed 21 Jan 2021

  4. Debugging with GDB: GDB/MI. https://sourceware.org/gdb/onlinedocs/gdb/GDB_002fMI.html. Accessed 21 Jan 2021

  5. GDB: The GNU Project Debugger. https://www.gnu.org/software/gdb/. Accessed 14 Oct 2020

  6. GitHub. https://github.com/. Accessed 18 Jan 2021

  7. Oracle VM VirtualBox. https://virtualbox.org/. Accessed 20 Apr 2021

  8. PVS-Studio. https://www.viva64.com/en/pvs-studio/. Accessed 18 Jan 2021

  9. Radare2 - A free/libre toolchain for easing several low level tasks like forensics, software reverse engineering, exploiting, debugging. https://rada.re/n/radare2.html. Accessed 21 Jan 2021

  10. Travis-CI. https://travis-ci.com/. Accessed 18 Jan 2021

  11. Valgrind: an instrumentation framework for building dynamic analysis tools. https://valgrind.org/. Accessed 21 Jan 2021

  12. Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1–6:39 (2018). https://doi.org/10.1145/3158668

  13. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008). google-Books-ID: 5dvxCwAAQBAJ

    Google Scholar 

  14. Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 331–346. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_23

    Chapter  MATH  Google Scholar 

  15. Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Int. J. Softw. Tools Technol. Transf. 14(1), 53–72 (2012)

    Article  Google Scholar 

  16. Boyer, B., Corre, K., Legay, A., Sedwards, S.: Plasma-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) Quantitative Evaluation System, pp. 160–164. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_12

    Chapter  Google Scholar 

  17. Bradley, M., Cassez, F., Fehnker, A., Given-Wilson, T., Huuck, R.: High performance static analysis for industry. Electron. Notes Theor. Comput. Sci. 289, 3–14 (2012)

    Article  Google Scholar 

  18. Bradley, M., Cassez, F., Fehnker, A., Given-Wilson, T., Huuck, R., Junker, M.: Goannasmt-a static analyzer with smt-based refinement (2012)

    Google Scholar 

  19. Cadar, C., et al.: Symbolic execution for software testing in practice: preliminary assessment. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, 21–28 May 2011, pp. 1066–1071. ACM (2011). https://doi.org/10.1145/1985793.1985995

  20. Chockler, H., Ivrii, A., Matsliah, A., Rollini, S.F., Sharygina, N.: Using cross-entropy for satisfiability. In: Shin, S.Y., Maldonado, J.C. (eds.) Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC 2013, Coimbra, Portugal, 18–22 March 2013, pp. 1196–1203. ACM (2013). https://doi.org/10.1145/2480362.2480588

  21. Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 168–176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_15

    Chapter  MATH  Google Scholar 

  22. D’Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469–484 (2015). https://doi.org/10.1007/s10009-015-0383-0

  23. David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015). https://doi.org/10.1007/s10009-014-0361-y

  24. David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of Herschel revisited using statistical model checking. Int. J. Softw. Tools Technol. Transfer 17(2), 187–199 (2014). https://doi.org/10.1007/s10009-014-0331-4

    Article  Google Scholar 

  25. Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Int. J. Softw. Tools Technol. Transfer (STTT) 2(4), 366–381 (2000)

    Article  Google Scholar 

  26. Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_24

    Chapter  MATH  Google Scholar 

  27. Hoeffding, W.: Probability Inequalities for Sums of Bounded Random Variables, pp. 409–426. Springer, New York (1994). https://doi.org/10.1007/978-1-4612-0865-5_26

  28. Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 576–591. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_38

    Chapter  Google Scholar 

  29. Kroening, D., Tautschnig, M.: CBMC - C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 389–391. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_26

    Chapter  Google Scholar 

  30. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) Runtime Verification, pp. 122–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  31. Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478–504. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91908-9_23

    Chapter  Google Scholar 

  32. Legay, A., Nowotka, D., Poulsen, D.B., Tranouez, L.-M.: Statistical model checking of LLVM code. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 542–549. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7_32

    Chapter  Google Scholar 

  33. Legay, A., Sedwards, S., Traonouez, L.M.: Plasma lab: a modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, pp. 77–93. Springer International Publishing, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_6

    Chapter  Google Scholar 

  34. Li, J., Dureja, R., Pu, G., Rozier, K.Y., Vardi, M.Y.: SimpleCAR: an efficient bug-finding tool based on approximate reachability. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 37–44. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_5

    Chapter  Google Scholar 

  35. Mignogna, A., Mangeruca, L., Boyer, B., Legay, A., Arnold, A.: Sos contract verification using statistical model checking. In: Larsen, K.G., Legay, A., Nyman, U. (eds.) Proceedings 1st Workshop on Advances in Systems of Systems, AiSoS 2013, Rome, Italy, 16th March 2013. EPTCS, vol. 133, pp. 67–83 (2013). https://doi.org/10.4204/EPTCS.133.7

  36. Ngo, V.C., Legay, A., Joloboff, V.: PSCV: a runtime verification tool for probabilistic SystemC models. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 84–91. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_5

    Chapter  Google Scholar 

  37. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46–57. IEEE, Providence, RI, USA, September 1977. http://ieeexplore.ieee.org/document/4567924/

  38. Raad, A., Berdine, J., Dang, H.H., Dreyer, D., O’Hearn, P., Villard, J.: Local reasoning about the presence of bugs: Incorrectness separation logic. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification, pp. 225–252. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_14

    Chapter  Google Scholar 

  39. Švejda, J., Berger, P., Katoen, J.-P.: Interpretation-based violation witness validation for C: NITWIT. TACAS 2020. LNCS, vol. 12078, pp. 40–57. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45190-5_3

    Chapter  Google Scholar 

  40. Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3576, pp. 429–433. Springer, Cham (2005). https://doi.org/10.1007/11513988_43

  41. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow/simulink verification. Formal Methods Syst. Design 43(2), 338–367 (2013). https://doi.org/10.1007/s10703-013-0195-3

Download references

Author information

Authors and Affiliations

  1. UCLouvain, Louvain-La-Neuve, Belgium

    Antoine Chenoy, Fabien Duchene, Thomas Given-Wilson & Axel Legay

Authors
  1. Antoine Chenoy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabien Duchene
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thomas Given-Wilson
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fabien Duchene .

Editor information

Editors and Affiliations

  1. Leiden University, Leiden, The Netherlands

    Alfons Laarman

  2. University of Salzburg, Salzburg, Austria

    Ana Sokolova

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chenoy, A., Duchene, F., Given-Wilson, T., Legay, A. (2021). C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs. In: Laarman, A., Sokolova, A. (eds) Model Checking Software. SPIN 2021. Lecture Notes in Computer Science(), vol 12864. Springer, Cham. https://doi.org/10.1007/978-3-030-84629-9_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-84629-9_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-84628-2

  • Online ISBN: 978-3-030-84629-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation