Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.
KeywordsSoftware Model CheckingSymbolic ExecutionState ExplosionAbstractionTest Case Generations
Henzinger, T.A., Jhala, R., Majumdar, R. and Sutre G. (2002) Lazy Abstraction. Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, 16-18 January 2002, 58-70. https://doi.org/10.1145/503272.503279
Louden, K.C. (1993) Programming Languages Principles and Practice. URL.
Baier, C. and Katoen, J. (2008) Principle of Model Checking. MIT Press, Cambridge.
Aggarwal, K.K. and Yogesh, S. (2001) Software Engineering. 3rd Edition, New Age International Ltd, New Delhi.
Van-Hung, D. (2005) Model-Checking and the SPIN Model Checker. International Institute for Software Technology, Macau.
Mount, S. (2013) A Language-Independent Static Checking System for Coding Conventions. Ph.D. Thesis, University of Wolverhampton, Wolverhampton. https://www.semanticscholar.org/paper/A-language-independent-static-checking-system-for-Mount/a13e0e45b0c16ac8dda081666b9d2037c44e6b10
Li, Y., Jiang, X., Zhang, Y., Xie, T. and Zhang, L. (2017) An Empirical Study on the limitations of Static Code Analysis for Vulnerability Detection. IEEE Transactions on Software Engineering, 43, 462-477.
Abrial, J. (2009) Modelling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge.
Clarke, E.M. (2008) The Birth of Model Checking. In: Grumberg, O. and Veith, H., Eds., 25 Years of Model Checking, Springer, Berlin, 1-26.
Strunk, E.A., Aiello, M.A. and Knight, J.C. (2006) A Survey of Tools for Model Checking and Model-Based Development. Technical Report, Department of Computer Science, University of Virginia, Charlottesville.
Jhala, R. and Majumdar, R. (2009) Software Model Checking. ACM Computing Surveys, 41, 1-54. https://doi.org/10.1145/1592434.1592438
Ben-Ari, M. (2008) Principles of SPIN Model Checker. Springer-Verlag, London.
Valero, M. (2005) Modal Abstraction and Replication of Processes with Data. Springer, Berlin. https://pdfs.semanticscholar.org/804b/02fd88d199360b65fb6efe13e93e84428596.pdf
Queille, J.P. and Sifakis, J. (1982) Specification and Verification of Concurrent System in CESAR. In: Dezani-Ciancaglini, M. and Montanari, U. Eds., Programming 1982: International Symposium on Programming, Springer, Berlin, 337-351. https://link.springer.com/chapter/10.1007/3-540-11494-7_22 https://doi.org/10.1007/3-540-11494-7_22
Clarke, E.M., Emerson, E.A. and Sistla, A.P. (1986) Automatic Verification of Finite-StateConcurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8, 244-263. https://doi.org/10.1145/5397.5399
Esparza, J. (1994) Model Checking Using Net Unfolding. Science of Computer Programming, 23, 151-195. https://doi.org/10.1016/0167-6423(94)00019-0
McMillan, K.L. (1992) Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. Thesis, Carnegie Mellon University, Pittsburgh, 1-212.
Yin, X. (2006) An Introduction to the SPIN Model Checker. Tools for Model Checking and Model-Based Development Project Report: Tool Description and Analysis.
Biere, A. (2008) Tutorial on Model Checking: Modelling and Verification in Computer Science. In: Horimoto, K., Regensburger, G., Rosenkranz, M. and Yoshida, H., Eds., AB 2008: Algebraic Biology, Lecture Notes in Computer Science, Springer, Berlin, 16-21. https://link.springer.com/chapter/10.1007/978-3-540-85101-1_2 https://doi.org/10.1007/978-3-540-85101-1_2
Khurshid, S., Pasareanu, C.S. and Visser, W. (2003) Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H. and Hatcliff, J., Eds., TACAS 2003: Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, 553-568. https://doi.org/10.1007/3-540-36577-X_40
Armando, A., Mantovani, J. and Platania, L. (2006) Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. In: Valmari, A., Ed., SPIN 2006: Model Checking Software, Springer, Berlin, 146-162. https://doi.org/10.1007/11691617_9
Yang, Z., Wang, C., Gupta, A. and Ivančić, F. (2008) Model Checking Sequential Software Programs via Mixed Symbolic Analysis. ACM Transaction on Design Automation of Electronic System, 14, 1-26. https://doi.org/10.1145/1455229.1455239
Wehrle, M. and Kupferschmid, S. (2010) Context-Enhanced Directed Model Checking. In: Van De Pol, J. and Weber, M., Eds., SPIN 2010: Model Checking Software, Springer, Berlin, 88-105. https://doi.org/10.1007/978-3-642-16164-3_7 https://link.springer.com/chapter/10.1007/978-3-642-16164-3_7
Eyer, D. and Stahlbauer, A. (2013) BDD-Based Software Model Checking with CPACHECKER. In: Kučera, A., Henzinger, T.A., Nešetřil, J., Vojnar, T. and Antoš, D., Eds., MEMICS 2012: Mathematical and Engineering Methods in Computer Science, Springer, Berlin, 1-11. https://doi.org/10.1007/978-3-642-36046-6_1 https://link.springer.com/chapter/10.1007/978-3-642-36046-6_1
Noureddine, M. and Zaraket, F.A. (2016) Model Checking Software with First Order Logic Specifications Using AIG Solvers. IEEE Transactions on Software Engineering, 42, 741-763. https://scholar.google.com/citations?user=iLJ3TyQAAAAJ&hl=en https://doi.org/10.1109/TSE.2016.2520468
Cousot, P. (2001) Abstract Interpretation Based Formal Methods and Future Challenge. https://www.di.ens.fr/~cousot/publications.www/Cousot-LNCS2000-sv-sb.pdf
Abraham, E. and Kremer, G. (2017) Satisfiability Checking: Theory and Application. Springer International Publishing, New York.
Ball, T., Podelski, A. and Rajamani, S.K. (2000) Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T. and Yi, W., Eds., TACAS 2001: Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, 268-283. https://link.springer.com/chapter/10.1007/3-540-45319-9_19 https://doi.org/10.1007/3-540-45319-9_19
Ball, T., Majumdar, R., Millstein, T. and Rajamani, S.K. (2001) Automatic Predicate Abstraction of C Programs. Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, Snowbird, June 2001, 203-213. https://doi.org/10.1145/378795.378846
Flanagan, C. and Qadeer, S. (2002) Predicate Abstraction for Software Verification. Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming, Portland, 16-18 January 2002, 191-202. https://doi.org/10.1145/503272.503291
Fehnker, A., Brauer, J., Huuck, R. and Seefried, S. (2008) Goanna: Syntactic Software Model Checking. In: Cha, S., Choi, J.Y., Kim, M., Lee, I. and Viswanathan, M., Eds., ATVA 2008: Automated Technology for Verification and Analysis, Springer, Berlin, 216-221. https://link.springer.com/chapter/10.1007/978-3-540-88387-6_17
Griesmayer, A. (2007) Debugging Software from Verification to Repair. Ph.D. Thesis, Graz University of Technology, Austria, 1-108
Li, Y. (2014) Symbolic Abstraction with SMT Solvers. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming, San Diego, 22-24 January 2014, 607-618. https://doi.org/10.1145/2535838.2535857
Lomuscio, A. and Michaliszyn, J. (2015) Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions. Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent, Istanbul, 4-8 May 2015, 189-198.
Clarke, E., Biere, A., Rami, R. and Zhu, Y. (2001) Bounded Model Checking Using Satisfiability Solving. Formal Method in System Design, 19, 7-34. https://doi.org/10.1023/A:1011276507260
Merz, F., Falke, S. and Sinz, C. (2012) LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., Müller, P. and Podelski, A., Eds., VSTTE 2012: Verified Software: Theories, Tools, Experiments, Springer, Berlin, 146-161. https://doi.org/10.1007/978-3-642-27705-4_12
Peled, D. (2001) Model Checking. Department of Computer Science, Bar llan University, Ramat Gan.
Guo, H.Y., Wu, M., Zhou, L.D., Hu, G., Yang, J.F. and Zhang L. (2011) Practical Software Model Checking via Dynamic Interface Reduction. Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, Cascais, 23-26 October 2011, 265-278. https://doi.org/10.1145/2043556.2043582
Nguyen, V.Y. and Ruys, T.C. (2013) Selected Dynamic Issues in Software Model Checking. International Journal on Software Tools for Technology Transfer, 15, 337-362. https://doi.org/10.1007/s10009-012-0261-y
Gupta, A., Kahlon, V., Qadeer, S. and Touili, T. (2018) Model Checking Concurrent Programs. In: Clarke, E., Henzinger, T., Veith, H. and Bloem, R., Eds., Handbook of Model Checking, Springer, Cham, 573-611. https://doi.org/10.1007/978-3-319-10575-8_18
Santos, I.S., Rocha, L.S., Santos-Neto, P.A. and Andrade, R.M.C. (2016) Model Verification of Dynamic Software Product Lines. Proceedings of the XXX Brazilian Symposium on Software Engineering, Maringá, 19-23 September 2016, 113-122. https://doi.org/10.1145/2973839.2973852
Avgerinos, T., Rebert, A., Cha, S.K. and Brumley, D. (2014) Enhancing Symbolic Execution with Veritesting. Proceedings of the 36th International Conference on Software Engineering, Hyderabad, 31 May-7 June 2014, 1083-1094. https://doi.org/10.1145/2568225.2568293
Bohme, M., Pham, V.T. and Roychoudhury, A. (2017) Coverage-Based Greybox Fuzzing as Markov Chain. IEEE Transactions on Software Engineering, 45, 489-506. https://doi.org/10.1109/TSE.2017.2785841
Gulzar, M.A., Musuvathi, M. and Kim, M. (2020) BigTest: A Symbolic Execution Based Systematic Test Generation Tool for Apache Spark. Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Companion Proceedings, Seoul South, 27 June-19 July 2020, 61-64. https://doi.org/10.1145/3377812.3382145
Chalupa, M., Jasek, T., Movak, J., Rechtackova, A., Sokova, V. and Strejcek, J. (2021) Symbiotic 8: Beyond Symbolic Execution. In: Groote, J.F. and Larsen, K.G., Eds., TACAS 2021: Tools and Algorithms for the Construction and Analysis of Systems, Springer, Cham, 453-457. https://doi.org/10.1007/978-3-030-72013-1_31
Mrazek, J., Bauch, P., Lauko, H. and Barnat, J. (2016) SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In: Bošnački, D. and Wijs, A., Eds., SPIN 2016: Model Checking Software, Springer, Cham, 208-213. https://doi.org/10.1007/978-3-319-32582-8_14
Visser, W., Pasareanu, C.S. and Khurshid, S. (2004) Test Input Generation with Java Pathfinder. ACM SIGSOFT Software Engineering Notes, 29, 97-107. https://doi.org/10.1145/1013886.1007526
Penczek, W., Szreter, M., Gerth, R. and Kuiper, R. (2000) Improving Partial Order Reductions for Universal Branching Time Properties. Fundameta Informaticae, 43, 245-267. https://doi.org/10.3233/FI-2000-43123413
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L. and Hwang, L.J. (1992) Symbolic Model Checking: 1020 States and Beyond. Information and Computation, 98, 142-170. https://doi.org/10.1016/0890-5401(92)90017-A
Havelund, K. and Pressburger, T. (1999) Model Checking Java Programs Using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2, 366-381. https://doi.org/10.1007/s100090050043
Cadar, C., Dunbar, D. and Engler, D.R. (2008) KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, San Diego, 8-10 December 2008, 209-224.
Clarke, E.M., Grumberg, O., Kroening D., Peled, D. and Veith H. (2018) Model Checking. 2nd Edition, MIT Press, Cambridge.
McMillan, K.L. (1999) Symbolic Model Checking. In: Inan, M.K. and Kurshan, R.P., Eds., Verification of Digital and Hybrid Systems, Springer, Berlin, 117-137. https://doi.org/10.1007/978-3-642-59615-5_6
Godefroid, P. (1996) Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Berlin. https://doi.org/10.1007/3-540-60761-7
Sen, K., Marinov, D., Agha, G. and Sridharan, M. (2016) Guiding Symbolic Execution towards Unexplored Code. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications, Amsterdam, 2-4 November 2016, 753-771.
Bao, X., Yin, H., Chen, X. and Zhang, L. (2018) Speeding Up Symbolic Model Checking with Machine Learning. Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, Montpellier, 3-7 September 2018, 570-580.
Ma, L., Zhang, F.Y., et al. (2018) DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems. ArXiv: 1803.07519.
Durrelli, V.H.S., Durelli, R.S., Borges, S.S., Endo, A.T., Eler, M.M., Dias, D.R.C. and Guimaraes, M.P. (2019) Machine Learning Applied to Software Testing: A Systematic Mapping Study. IEEE Transactions on Realiability, 68, 1189-1212. https://doi.org/10.1109/TR.2019.2892517
Vardhan, A., Sen, K., Viswanathan, M. and Agha, G. (2004) Learning to Verify Safety Properties. In: Davies, J., Schulte, W. and Barnett, M., Eds., ICFEM 2004: Formal Methods and Software Engineering, Springer, Berlin, 274-289. https://doi.org/10.1007/978-3-540-30482-1_26
Kalyan, A., Mohta, A., Polozov, O., Batra, D., Jain, P. and Gulwani, S. (2018) Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples. ArXiv: 1804.01186. https://arxiv.org/abs/1804.01186
Gennari, J., Gurfinkel, A., Kahsai, T., Navas, J.A. and Schwartz, E.J. (2018) Executable Counterexamples in Software Model Checking. In: Piskac, R. and Rümmer, P., Eds., VSTTE 2018: Verified Software: Theories, Tools and Experiments, Vol. 11294, Springer, Cham, 17-37. https://doi.org/10.1007/978-3-030-03592-1_2
Utting, M. and Legeard, B. (2006) Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann, San Francisco.
Havelund, K. and Rosu, G. (2002) Monitoring Programs Using Rewriting. Proceedings of the 14th International Conference on Computer Aided Verification, Copenhagen, 27-31 July 2002, 450-462.
Pacheco, C., Lahiri, S.K., Ernst, M.D. and Ball, T. (2007) Feedback-Directed Random Test Generation. 29th International Conference on Software Engineering, Minneapolis, MN, 20-26 May 2007, 75-84. https://doi.org/10.1109/ICSE.2007.37
Harman, M. and Sthamer, H. (2002) Search-Based Software Testing. Proceedings of the 2002 International Symposium on Software Testing and Analysis, Roma, 22-24 July 2002, 249-258.
King, J.C. (1976) Symbolic Execution and Program Testing. Communications of the ACM, 19, 385-394. https://doi.org/10.1145/360248.360252
Liang, G., Liao, L., Xu, X., Du, J., Li, G. and Zhao, H. (2013) Effective Fuzzing Based on Dynamic Taint Analysis. 2013 Ninth International Conference on Computational Intelligence and Security, Emeishan, 14-15 December 2013, 615-619. https://doi.org/10.1109/CIS.2013.135
Kwiatkowska, M., Norman, G. and Parker, D. (2018) Probabilistic Model Checking: Advances and Applications. In: Drechsler, R., Ed., Formal System Verification, Springer, Cham, 73-121. https://doi.org/10.1007/978-3-319-57685-5_3
Sen, K., Marinov, D. and Agha, G. (2005) CUTE: A Concolic Unit Testing Engine for C. Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE-13), Chicago, 5-9 September 2005, 263-272.
Satpathy, M. and Ramesh, S. (2007) Test Case Generation from Formal Models through Abstraction Refinement and Model Checking. Proceedings of the 3rd International Workshop on Advances in Model-Based Testing, London, 9-12 July 2007, 85-94. https://doi.org/10.1145/1291535.1291544
Emerson, E.A. and Namjoshi, K.S. (1998) Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8, 244-263.
Lamport, L. (1986) On Interprocess Communication. Distributed Computing, 1, 77-85. https://doi.org/10.1007/BF01786227
Alur, R., Bodík, R., Juniwal, G. and Seshia, S.A. (2015) Synthesis of Cyber-Physical Systems. Proceedings of the IEEE, 103, 1589-1609.
Gurfinkel, A. and Chaki, S. (2015) Combining Static Analysis and Model Checking for Program Analysis. Formal Methods in System Design, 47, 62-91.
Zhang, L., Chen, Y., Zhang, Y. and Liu, Y. (2020) A Critical Survey of Machine Learning-Assisted Verification. IEEE Transactions on Software Engineering, 47, 1064-1087.
Pei, K., Cao, Y., Yang, J. and Jia, Z. (2017) Deep Learning-Based Software-Defined Networking for IoT Security. IEEE Network, 31, 80-85.
Gao, Y., Wei, Y., Sun, J. and Zhang, X. (2019) Learning-Based Abstraction Refinement for Software Model Checking. Frontiers of Information Technology and Electronic Engineering, 20, 372-382.
Zhang, X., Liu, Y., Huang, L. and Zhang, Y. (2021) Reinforcement Learning-Based Heuristic for Accelerating Software Model Checking. Journal of Systems and Software, 174, Article ID: 110950.