Finding More Bugs with Software Model Checking using Delta Debugging
https://doi.org/10.15514//ISPRAS-2023-35(3)-11
Abstract
Many verification tasks in model checking (one of the formal software verification approaches) can’t be solved within bounded time requirements due to combinatorial state space explosion. In order to find a bug in the verified program in a given time, a simplified version of it can be analyzed. This paper presents DD** algorithms (based on the Delta Debugging approach) to iterate over simplified versions of the given program. These algorithms were implemented in software-verification tool CPAchecker. Our experiments showed that this technique might be used to find new bugs in real software.
Supporting agencies: The author thanks his colleagues Anton Vasilyev and Vadim Mutilin for their useful advices on the article topic.
About the Author
Oleg Maximovich PETROV
Lomonosov Moscow State University, Ivannikov Institute for System Programming of the Russian Academy of Sciences.
Russian Federation
Russian Federation
Senior laboratory assistant and a master of the Faculty of Computational Mathematics and Cybernetics.
References
1. A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.
2. D. Beyer and M. E. Keremoglu, “CPAchecker: A tool for configurable software verification,” in Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23. Springer, 2011, pp. 184–190.
3. D. Beyer, S. Gulwani, and D. A. Schmidt, Combining Model Checking and Data-Flow Analysis. in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, pp. 493–540.
4. A. Khoroshilov, V. Mutilin, A. Petrenko, and V. Zakharov, “Establishing linux driver verification process,” in Perspectives of Systems Informatics: 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers 7. Springer, 2010, pp. 165–176.
5. I. S. Zakharov, M. U. Mandrykin, V. S. Mutilin, E. Novikov, A. K. Petrenko, and A. V. Khoroshilov, “Configurable toolset for static verification of operating systems kernel modules,” Programming and Computer Software, vol. 41, pp. 49–64, 2015.
6. D. Beyer, “Software verification: 10th comparative evaluation (SVCOMP 2021),” Tools and Algorithms for the Construction and Analysis of Systems, vol. 12652, pp. 401 – 422, 2021.
7. “Progress on software verification: SV-COMP 2022,” in International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2022.
8. “Competition on software verification and witness validation: SVCOMP 2023,” in International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2023.
9. N. Piterman and A. Pnueli, Temporal Logic and Fair Discrete Systems, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, p. 27–73.
10. A. V. Khoroshilov, M. U. Mandrykin, and V. S. Mutilin, “Introduction to CEGAR — counter-example guided abstraction refinement”, Trudy ISP RAN/Proc. ISP RAS, vol. 24, 2013, (in Russian).
11. D. A. Peled, Partial-Order Reduction, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018.
12. E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla, “Symmetry reductions in model checking,” in International Conference on Computer Aided Verification, 1998.
13. S. Chaki and A. Gurfinkel, BDD-Based Symbolic Model Checking, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, p. 219–245.
14. A. Biere and D. Kröning, SAT-based model checking, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, ch. 10, pp. 277–303.
15. F. Nejati, A. A. A. Ghani, N. K. Yap, and A. B. Jafaar, “Handling state space explosion in component-based software verification: A review,” IEEE Access, vol. 9, pp. 77 526–77 544, 2021.
16. S. Apel, D. Beyer, V. O. Mordan, V. S. Mutilin, and A. Stahlbauer, “On-the-fly decomposition of specifications in software model checking,” Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016.
17. T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. A. Sanvido, “Extreme model checking,” in Theory and Practice, 2003.
18. D. Beyer, S. Lo¨we, E. Novikov, A. Stahlbauer, and P. Wendler, “Precision reuse for efficient regression verification,” in ESEC/FSE 2013, 2013.
19. D. Beyer, T. A. Henzinger, M. E. Keremoglu, and P. Wendler, “Conditional model checking: a technique to pass information between verifiers,” in SIGSOFT FSE, 2012.
20. D. Beyer and S. Kanav, “CoVeriTeam: On-demand composition of cooperative verification systems,” in International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2022.
21. M. Weiser, “Program slicing,” IEEE Transactions on Software Engineering, vol. SE-10, no. 4, pp. 352–357, 1984.
22. M. Chalupa and J. Strejček, “Evaluation of program slicing in software verification,” in International Conference on Integrated Formal Methods, 2019.
23. P. Andrianov, V. Mutilin, M. Mandrykin, and A. Vasilyev, “CPA-BAM-Slicing: Block-abstraction memoization and slicing with region-based dependency analysis,” in Tools and Algorithms for the Construction and Analysis of Systems, D. Beyer and M. Huisman, Eds. Cham: Springer International Publishing, 2018, pp. 427–431.
24. M. Spiessl, “Configurable software verification based on slicing abstractions,” Master’s thesis, Ludwig-Maximilians-Universita¨t Mu¨nchen (LMU Munich), Mu¨nchen, Germany, Jun. 2018.
25. A. Zeller and R. Hildebrandt, “Simplifying and isolating failure-inducing input,” IEEE Trans. Software Eng., vol. 28, pp. 183–200, 2002.
26. G. Misherghi and Z. Su, “HDD: hierarchical delta debugging,” Proceedings of the 28th international conference on Software engineering, 2006.
27. D. Vince, R. Hodován, D. Bársony, and Á. Kiss, “The effect of hoisting on variants of Hierarchical Delta Debugging,” Journal of Software: Evolution and Process, vol. 34, 2022.
28. C. G. Kalhauge and J. Palsberg, “Binary reduction of dependency graphs,” Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019.
29. D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, and T. Lemberger, “Verification witnesses,” ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 31, pp. 1 – 69, 2022.
30. M. Dangl, S. Löwe, and P. Wendler, “CPAchecker with support for recursive programs and floating-point arithmetic,” in Tools and Algorithms for the Construction and Analysis of Systems, C. Baier and C. Tinelli, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015, pp. 423– 425.
31. E. Novikov and I. Zakharov, “Towards automated static verification of GNU C programs,” in Perspectives of System Informatics: 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers 11. Springer, 2018, pp. 402–416.
32. A. A. Vasilyev and V. S. Mutilin, “Predicate extension of symbolic memory graphs for the analysis of memory safety correctness,” Programming and Computer Software, vol. 46, pp. 747 – 754, 2020.
Review
For citations:
PETROV O.M. Finding More Bugs with Software Model Checking using Delta Debugging. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2023;35(3):151-162. https://doi.org/10.15514//ISPRAS-2023-35(3)-11
Email this article 