Towards automatic deductive verification of C programs with sisal loops using the C-lightVer system

D. A. Kondratyev

Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 372-393.

Résumé

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

Détail

Keywords: deductive verification, C-lightVer, cloud parallel programming system, symbolic method of verification of definite iterations, loop invariant
Mots-clés : ACL2.

Bibliographie

[1] I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, D. A. Kondratyev, “Automatic C Program Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 48:7 (2014), 407–414 | DOI

[2] D. A. Kondratyev, A. V. Promsky, “Developing a self-applicable Verification system. Theory and practice”, Automatic Control and Computer Sciences, 49:7 (2015), 445–452 | DOI

[3] D. Kondratyev, “Implementing the Symbolic Method of Verification in the C-Light Project”, Perspectives of System Informatics, LNCS, 10742, Springer, 2018, 227–240

[4] D. A. Kondratyev, I. V. Maryasov, V. A. Nepomniaschy, “The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination”, Automatic Control and Computer Sciences, 53:7 (2019), 653–662 | DOI

[5] D. A. Kondratyev, A. V. Promsky, “The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs”, Automatic Control and Computer Sciences, 54:7 (2020), 728–739 | DOI | MR

[6] C. A. R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM, 12:10 (1969), 576–580 | DOI | Zbl

[7] K. R. Apt, E. R. Olderog, “Fifty years of Hoare's logic”, Formal Aspects of Computing, 31:6 (2019), 751–807 | DOI | MR | Zbl

[8] R. Hahnle, M. Huisman, “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools”, Computing and Software Science, LNCS, 10000, Springer, 2019, 345–373

[9] K. R. Apt, E.-R. Olderog, “Assessing the Success and Impact of Hoare's Logic”, Theories of Programming: The Life and Works of Tony Hoare, 2021, 41–76 | DOI

[10] V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhailov, A. V. Promskii, “Towards Verification of C programs. C-light language and its formal semantics”, Programming and Computer Software, 28:6 (2002), 314–323 | DOI | MR

[11] V. A. Nepomniaschy, I. S. Anureev, A. V. Promskii, “Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language”, Programming and Computer Software, 29:6 (2003), 338–350 | DOI | MR | Zbl

[12] V. A. Nepomniaschy, “Symbolic method of Verification of definite iterations over altered data structures”, Programming and Computer Software, 31:1 (2005), 1–9 | DOI | MR | Zbl

[13] M. Moriconi, R. L. Schwartz, “Automatic construction of Verification condition generators from hoare logics”, International Colloquium on Automata, Languages, and Programming, LNCS, 115, Springer, 1981, 363–377

[14] J. S. Moore, “Milestones from the Pure Lisp Theorem Prover to ACL2”, Formal Aspects of Computing, 31:6 (2019), 699–732 | DOI | MR | Zbl

[15] V. Kasyanov, E. Kasyanova, “Methods and System for Cloud Parallel Programming”, Proceedings of the 21st International Conference on Enterprise Information Systems, v. 1, 2019, 623–629 | DOI

[16] V. N. Kasyanov, A. P. Stasenko, “Sisal 3.2 Language Structure Decomposition”, Proceedings of the European Computing Conference, LNEE, 28, Springer, 2009, 533–543

[17] A. Stasenko, “Sisal 3.2 Language Features Overview”, International Conference on Parallel Computing Technologies, LNCS, 6873, Springer, 2011, 110–124

[18] V. Kasyanov, “Sisal 3.2: functional language for scientific parallel programming”, Enterprise Information Systems, 7:2 (2013), 227–236 | DOI

[19] J. T. Feo, D. C. Cann, R. R. Oldehoeft, “A report on the sisal language project”, Journal of Parallel and Distributed Computing, 10:4 (1990), 349–366 | DOI

[20] J. L. Gaudiot, T. DeBoni, J. Feo, W. Bohm, W. Najjar, P. Miller, “The Sisal Project: Real World Functional Programming”, Compiler Optimizations for Scalable Parallel Systems, LNCS, 1808, Springer, 2001, 45–72

[21] K. Pyzhov, R. Idrisov, “Back-end translator for Sisal 3.1 compiler”, Bulletin of the Novosibirsk Computing Center, 2013, no. 35, 101–119

[22] D. A. Kondratyev, A. V. Promsky, “Towards Verification of scientific and engineering programs. The CPPS project”, Journal of Computational Technologies, 25:5 (2020), 91–106

[23] J. Dean, S. Ghemawat, “MapReduce: simplified data processing on large clusters”, Proceedings of the 6th conference on Symposium on Operating Systems Design Implementation, v. 6, 2004

[24] M. Kaufmann, J. S. Moore, “Iteration in ACL2”, Proceedings of the Sixteenth International Workshop on the ACL2eorem Prover and its Applications, EPTCS, 327, 2020, 16–31 | DOI

[25] S. Blom, S. Darabi, M. Huisman, M. Safari, “Correct program parallelisations”, International Journal on Software Tools for Technology Transfer, 23:5 (2021), 741–763 | DOI

[26] B. Jacobs, J. Kiniry, M. Warnier, “Java Program Verification Challenges”, Formal Methods for Components and Objects, LNCS, 2852, Springer, 2003, 202–219

[27] D. R. Cok, “Reasoning about Functional Programming in Java and C++”, Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, 2018, 37–39 | DOI

[28] D. R. Cok, S. Tasiran, “Practical Methods for Reasoning About Java 8's Functional Programming Features”, Verified Software:eories, Tools, and Experiments, LNCS, 11294, Springer, 2018, 267–278

[29] ISO/IEC 14882:2020: Programming language C++, ISO/IEC, 2020

[30] ISO/IEC 9899:2011: Programming language C, ISO/IEC, 2011

[31] R. Krebbers, F. Wiedijk, “A Typed C11 Semantics for Interactive theorem Proving”, Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015, 15–27 | DOI

[32] M. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, D. Garg, “RefinedC: automating the foundational Verification of C code with refined ownership types”, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, 158–174 | DOI

[33] M. O. Myreen, M. J. C. Gordon, “Transforming Programs into Recursive Functions”, Electronic Notes ineoretical Computer Science, 240 (2009), 185–200 | DOI | Zbl

[34] R. Blanc, V. Kuncak, E. Kneuss, P. Suter, “An overview of the Leon Verification system: Verification by translation to recursive functions”, Proceedings of the 4th Workshop on Scala, 2013, 1–10 | Zbl

[35] A. Humenberger, M. Jaroschek, L. Kovacs, “Invariant Generation for Multi-Path Loops with Polynomial Assignments”, Verification, Model Checking, and Abstract Interpretation, LNCS, 10747, Springer, 2018, 226–246 | MR | Zbl

[36] S. Chakraborty, A. Gupta, D. Unadkat, “Diffy: Inductive Reasoning of Array Programs Using Difference Invariants”, Computer Aided Verification, LNCS, 12760, Springer, 2021, 911–935

[37] T. Tuerk, “Local reasoning about while-loops”, Proceedings of the Theory Workshop at VSTTE 2010, 2010, 29–39

[38] A. Blanchard, F. Loulergue, N. Kosmatov, “Towards Full Proof Automation in Frama-C Using Auto-active Verification”, NASA Formal Methods, LNCS, 11460, Springer, 2019, 88–105

[39] P. Baudin, F. Bobot, D. Buhler, L. Correnson, F. Kirchner, N. Kosmatov, A. Maroneze, V. Perrelle, V. Prevosto, J. Signoles, N. Williams, “The dogged pursuit of bug-free C programs: the Frama-C Software analysis platform”, Communications of the ACM, 64:8 (2021), 56–68 | DOI

[40] I. Attali, D. Caromel, A. Wendelborn, “A Formal Semantics and an Interactive Environment for Sisal”, Tools and Environments for Parallel and Distributed Systems, SOFT, 2, Springer, 1996, 229–256

[41] D. Kondratyev, A. Promsky, “Proof Strategy for Automated Sisal Program Verification”, Software Technology: Methods and Tools, LNCS, 11771, Springer, 2019, 113–120

[42] B. Beckert, T. Bingmann, M. Kiefer, P. Sanders, M. Ulbrich, A. Weigl, “Relational Equivalence Proofs Between Imperative and MapReduce Algorithms”, Verified Software. Theories, Tools, and Experiments, LNCS, 11294, Springer, 2018, 248–266

[43] G. Parthasarathy, P. Muller, A. Summers, “Formally Validating a Practical Verification Condition Generator”, Computer Aided Verification, LNCS, 12760, Springer, 2021, 704–727