Capabilities and Restrictions of Software Model Checkers
https://doi.org/10.15514/ISPRAS-2021-33(6)-1
Abstract
Software model checkers enable automatic detection of violations of specified requirements in programs as well as formal proof of correctness under certain assumptions. These tools actively evolve two last decades. They were already successfully applied to a bunch of industrial projects, first of all to kernels and drivers of various operating systems. This paper considers an interface of software model checkers, their unique capabilities as well as restrictions that prevent their large-scale usage on practice.
About the Author
Evgeny Mikhailovich NOVIKOV
Ivannikov Institute for System Programming of the RAS
Russian Federation
Russian Federation
PhD, Senior Researcher at the Software Engineering Department
References
1. P.E. Black, L. Badger et al. Dramatically reducing software vulnerabilities: report to the White House Office of Science and Technology Policy. Technical Report NISTIR 8151, National Institute of Standards and Technology, Gaithersburg, MD, 2016.
2. G. Klein, J. Andronick et al. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, volume 32, issue 1, 2014, pp. 1-70.
3. D. Efremov, M. Mandrykin, A. Khoroshilov. Deductive verification of unmodified Linux kernel library functions. Lecture Notes in Computer Science, vol. 11245, 2018, pp. 216-234.
4. D. Beyer. Competition on software verification. Lecture Notes in Computer Science, vol. 7214, 2012, pp. 504-524.
5. D. Beyer. Software verification: 10th comparative evaluation (SV-COMP 2021). Lecture Notes in Computer Science, vol. 12652, 2021, pp. 401–422.
6. Definitions and Rules of 10th International Competition on Software Verification. URL: https://sv-comp.sosy-lab.org/2021/rules.php, accessed 12.12.2021.
7. V. Mutilin, E. Novikov, A. Khoroshilov. Analysis of typical faults in Linux operating system drivers. Trudy ISP RAN/Proc. ISP RAS, vol. 22, 2012, pp. 349-374 (in Russian). https://doi.org/10.15514/ISPRAS-2012-22-19.
8. P. Andrianov. Analysis of correct synchronization of operating system components. Programming and Computer Software, vol. 46, issue 8, 2020, pp. 712-730. https://doi.org/10.1134/S0361768820080022.
9. I. Zakharov. A survey of high-performance computing for software verification. Communications in Computer and Information Science, vol. 779, 2017, pp. 196-208.
10. I. Zakharov, E. Novikov. Compositional environment modelling for verification of GNU C programs. In: Proc. of the Ivannikov Ispras Open Conference, 2018, pp. 39–44.
11. Exchange Format for Violation Witnesses and Correctness Witnesses. URL: https://github.com/sosy-lab/sv-witnesses, accessed 12.12.2021.
12. D. Beyer, M. Dangl et al. Correctness witnesses: exchanging verification results between verifiers. In Proc. of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016, pp. 326-337.
13. D. Beyer, M. Dangl et al. Witness validation and stepwise testification across software verifiers. In Proc. of the 10th Joint Meeting on Foundations of Software Engineering, 2015, pp. 721-733.
14. D. Beyer, M.E. Keremoglu. CPAchecker: a tool for configurable software verification. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 184–190.
15. R. Castaño, V. Braberman et al. Model checker execution reports. In Proc. of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017, pp. 200-205.
16. LCOV – the LTP GCOV extension. URL: https://github.com/linux-test-project/lcov, accessed 12.12.2021.
17. T. Ball, V. Levin, S.K. Rajamani. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, 2011, pp. 68-76.
18. Klever: a software verification framework. URL: https://forge.ispras.ru/projects/klever, accessed 12.12.2021.
19. E. Novikov and I. Zakharov. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402-416.
20. VerifierCloud Web Interface. URL: https://vcloud.sosy-lab.org, accessed 12.12.2021.
Review
For citations:
NOVIKOV E.M. Capabilities and Restrictions of Software Model Checkers. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(6):7-14. https://doi.org/10.15514/ISPRAS-2021-33(6)-1
Email this article 