nach oben

Automatic Control and Computer Sciences

Erschienen in:

01.12.2022

Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

verfasst von: D. A. Kondratyev

Erschienen in: Automatic Control and Computer Sciences | Ausgabe 7/2022

Einloggen, um Zugang zu erhalten

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The C-lightVer system for deductive verification of C programs has been developed at the Institute of Informatics Systems of the Siberian Branch of the Russian Academy of Sciences (IIS SB RAS). C-kernel is an intermediate verification language in this system. The cloud parallel programming system (CPPS) is also developed at the IIS SB RAS. Cloud Sisal is the input language of the CPPS system. The main feature of the CPPS system is the implicit parallel execution based on the automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is the automatic parallelization of such a superset of the C language that allows implementing automatic verification. Our solution is a superset of the C-kernel language such as the C-Sisal-kernel language. The first result presented in this article is an extension of C-kernel by Cloud-Sisal-kernel loops. As a consequence, the C-Sisal-kernel language is developed. The second result presented in this article is the extension of the C-kernel axiomatic semantics by an inference rule for Cloud-Sisal-kernel loops. This article also presents our approach to the problem of automating deductive verification in the case of definite iterations over data sequences. Such loops are called definite iterations. Our solution is a composition of a symbolic method of verification of definite iterations, verification condition metageneration, and mixed axiomatic semantics. The symbolic method of verification of definite iterations allows us to define inference rules for such loops without invariants. Symbolic replacement of definite iterations by recursive functions is the basis of this method. The resulting verification conditions using recursive functions correspond to the logical basis of the ACL2 prover. We use the ACL2 system based on computable recursive functions. Verification condition metageneration simplifies the implementation of new inference rules in the verification system. In some cases, the use of mixed axiomatic semantics leads to simpler verification conditions.

Vorheriger Artikel An Algorithm for Estimating the Signal Frequency at the Output of a Channel with a Controlled Information Flow under Phase Noise

Nächster Artikel Backtracking Algorithms for Constructing the Hamiltonian Decomposition of a 4-Regular Multigraph

Maryasov, I.V., Nepomniaschy, V.A., Promsky, A.V., and Kondratyev, D.A., Automatic C program verification based on mixed axiomatic semantics, Autom. Control Comput. Sci., 2014, vol. 48, no. 7, pp. 407–414. https://doi.org/10.3103/S0146411614070141CrossRef

Kondratyev, D.A. and Promsky, A.V., Developing a self-applicable verification system. Theory and practice, Autom. Control Comput. Sci., 2015, vol. 49, no. 7, pp. 445–452. https://doi.org/10.3103/S0146411615070123CrossRef

Kondratyev, D., Implementing the symbolic method of verification in the C-light project, Perspectives of System Informatics. PSI 2017,Petrenko, A. and Voronkov, A., Eds., Lecture Notes in Computer Science, vol. 10742, Cham: Springer, 2018, pp. 227–240. https://doi.org/10.1007/978-3-319-74313-4_17CrossRef

Kondratyev, D.A., Maryasov, I.V., and Nepomniaschy, V.A., The automation of C program verification by the symbolic method of loop invariant elimination, Autom. Control Comput. Sci., 2019, vol. 53, no. 7, pp. 653–662. https://doi.org/10.3103/S0146411619070101CrossRef

Kondratyev, D.A. and Promsky, A.V., The complex approach of the C-lightVer system to the automated error localization in C-programs, Autom. Control Comput. Sci., 2020, vol. 54, no. 7, pp. 728–739. https://doi.org/10.3103/S0146411620070093CrossRef

Hoare, C.A.R., An axiomatic basis for computer programming, Commun. ACM, 1969, vol. 12, no. 10, pp. 576–580. https://doi.org/10.1145/363235.363259CrossRefMATH

Apt, K.R. and Olderog, E.-R., Fifty years of Hoare’s logic, Formal Aspects Comput., 2019, vol. 31, no. 6, pp. 751–807. https://doi.org/10.1007/s00165-019-00501-3MathSciNetCrossRefMATH

Hähnle, R. and Huisman, M., Deductive software verification: From pen-and-paper proofs to industrial tools, Computing and Software Science, Steffen, B. and Woeginger, G., Eds., Lecture Notes in Computer Science, vol. 10000, Springer, 2019, pp. 345–373. https://doi.org/10.1007/978-3-319-91908-9_18

Apt, K.R. and Olderog, E.-R., Assessing the success and impact of Hoare’s logic, Theories of Programming: The Life and Works of Tony Hoare, Jones, C.B. and Misra, J., Eds., New York: Association for Computing Machinery, 2021, pp. 41–76. https://doi.org/10.1145/3477355.3477359CrossRefMATH

10.

Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promskii, A.V., Towards verification of C programs. C-light language and its formal semantics, Program. Comput. Software, 2002, vol. 28, no. 6, pp. 314–323.https://doi.org/10.1023/A:1021045909505MathSciNetCrossRef

11.

Nepomniaschy, V.A., Anureev, I.S., and Promskii, A.V., Towards verification of C programs: Axiomatic semantics of the C-kernel language, Program. Comput. Software, 2003, vol. 29, no. 6, pp. 338–350. https://doi.org/10.1023/B:PACS.0000004134.24714.e5MathSciNetCrossRefMATH

12.

Nepomniaschy, V.A., Symbolic method of verification of definite iterations over altered data structures, Program. Comput. Software, 2005, vol. 31, no. 1, pp. 1–9. https://doi.org/10.1007/s11086-005-0001-0MathSciNetCrossRefMATH

13.

Moriconi, M. and Schwartz, R.L., Automatic construction of verification condition generators from Hoare logics, Automata, Languages, and Programming. ICALP 1981, Even, S. and Kariv, O., Eds., Lecture Notes in Computer Science, vol. 115, Springer, 1981, pp. 363–377. https://doi.org/10.1007/3-540-10843-2_30CrossRefMATH

14.

Moore, J.S., Milestones from the Pure Lisp theorem prover to ACL2, Formal Aspects Comput., 2019, vol. 31, no. 6, pp. 699–732. https://doi.org/10.1007/s00165-019-00490-3MathSciNetCrossRefMATH

15.

Kasyanov, V. and Kasyanova, E., Methods and system for cloud parallel programming, Proc. 21st Int. Conference on Enterprise Information Systems, 2019, vol. 1, pp. 623–629. https://doi.org/10.5220/0007750506230629

16.

Kasyanov, V.N. and Stasenko, A.P., Sisal 3.2 language structure decomposition, Proc. European Computing Conference, Mastorakis, N., Mladenov, V., and Kontargyri, V., Eds., Lecture Notes in Electrical Engineering, vol. 28, Springer, 2009, pp. 533–543. https://doi.org/10.1007/978-0-387-85437-3_53

17.

Stasenko, A., Sisal 3.2 Language features overview, Parallel Computing Technologies. PaCT 2011, Malyshkin, V., Ed., Lecture Notes in Computer Science, vol. 6873, Springer, 2011, pp. 110–124. https://doi.org/10.1007/978-3-642-23178-0_10CrossRef

18.

Kasyanov, V., Sisal 3.2: Functional language for scientific parallel programming, Enterprise Inf. Syst., 2013, vol. 7, no. 2, pp. 227–236. https://doi.org/10.1080/17517575.2012.744854CrossRef

19.

Feo, J.T., Cann, D.C., and Oldehoeft, R.R., A report on the sisal language project, J. Parallel Distributed Comput., 1990, vol. 10, no. 4, pp. 349–366. https://doi.org/10.1016/0743-7315(90)90035-NCrossRef

20.

Gaudiot, J.-L., DeBoni, T., Feo, J., Böhm, W., Najjar, W., and Miller, P., The Sisal project: Real world functional programming, Compiler Optimizations for Scalable Parallel Systems,Pande, S. and Agrawal, D.P., Eds., Lecture Notes in Computer Science, vol. 1808, Springer, 2001, pp. 45–72. https://doi.org/10.1007/3-540-45403-9_2CrossRef

21.

Pyzhov, K. and Idrisov, R., Back-end translator for Sisal 3.1 compiler, Bull. Novosibirsk Comput. Center, 2013, no. 35, pp. 101–119.https://doi.org/10.31144/bncc.cs.2542-1972.2013.n35.p101-119

22.

Kondratyev, D.A. and Promsky, A.V., Towards verification of scientific and engineering programs. The CPPS project,Journal of Computational Technologies, 2020, vol. 25, no. 5, pp. 91–106. https://doi.org/10.25743/ICT.2020.25.5.008CrossRef

23.

Dean, J. and Ghemawat, S., MapReduce: Simplified data processing on large clusters, Proc. 6th Conf. on Symp. on Operating Systems Design & Implementation, 2004, vol. 6.

24.

Kaufmann, M. and Moore, J.S., Iteration in ACL2, Proc. Sixteenth Int. Workshop on the ACL2 Theorem Prover and Its Applications, ser. EPTCS, 2020, vol. 327, pp. 16–31. https://doi.org/10.4204/EPTCS.327.2

25.

Blom, S., Darabi, S., Huisman, M., and Safari, M., Correct program parallelisations,Int. J. Software Tools Technol. Transfer, 2021, vol. 23, no. 5, pp. 741–763. https://doi.org/10.1007/s10009-020-00601-zCrossRef

26.

Jacobs, B., Kiniry, J., and Warnier, M., Java program verification challenges, Formal Methods for Components and Objects, de Boer, F.S., Bonsangue, M.M., Graf, S., and de Roever, W.P., Eds., Lecture Notes in Computer Science, vol. 2852, Springer, 2003, pp. 202–219. https://doi.org/10.1007/978-3-540-39656-7_8

27.

Cok, D.R., Reasoning about Functional Programming in Java and C++, ISSTA ’18: Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, Amsterdam, 2018, New York: Association for Computing Machinery, 2018, pp. 37–39. https://doi.org/10.1145/3236454.3236483CrossRef

28.

Cok, D.R. and Tasiran, S., Practical methods for reasoning about Java 8’s functional programming features, in Verified Software: Theories, Tools, and Experiments. VSTTE 2018, Piskac, R. and Rümmer, P., Eds., Lecture Notes in Computer Science, vol. 11294, Springer, 2018, pp. 267–278. https://doi.org/10.1007/978-3-030-03592-1_15CrossRef

29.

ISO/IEC 14882:2020: Programming language C++. ISO/IEC, 2020.

30.

ISO/IEC 9899:2011: Programming language C. ISO/IEC, 2011.

31.

Krebbers, R. and Wiedijk, F., A typed C11 semantics for interactive theorem proving, CPP ’15: Proc. 2015 Conference on Certified Programs and Proofs, Mumbai, India, 2015, New York: Association for Computing Machinery, 2015, pp. 15–27. https://doi.org/10.1145/2676724.2693571

32.

Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., and Garg, D., RefinedC: automating the foundational verification of C code with refined ownership types, PLDI 2021: Proc. 42nd ACM SIGPLAN Int. Conference on Programming Language Design and Implementation, New York: Association for Computing Machinery, 2021, pp. 158–174. https://doi.org/10.1145/3453483.3454036

33.

Myreen, M.O. and Gordon, M.J.C., Transforming programs into recursive functions, Electron. Notes Theor. Comput. Sci., 2009, vol. 240, pp. 185–200. https://doi.org/10.1016/j.entcs.2009.05.052CrossRefMATH

34.

Blanc, R., Kuncak, V., Kneuss, E., and Suter, P., An overview of the Leon verification system: verification by translation to recursive functions, SCALA ’13: Proc. 4th Workshop on Scala, Montpellier, France, 2013, New York: Association for Computing Machinery, 2013, p. 1. https://doi.org/10.1145/2489837.2489838

35.

Humenberger, A., Jaroschek, M., and Kovács, L., Invariant generation for multi-path loops with polynomial assignments, Verification, Model Checking, and Abstract Interpretation. VMCAI 2018, Dillig, I. and Palsberg, J., Eds., Lecture Notes in Computer Science, vol. 10747, Springer, 2018, pp. 226–246. https://doi.org/10.1007/978-3-319-73721-8_11CrossRefMATH

36.

Chakraborty, S., Gupta, A., and Unadkat, D., Diffy: Inductive reasoning of array programs using difference invariants, Computer Aided Verification. CAV 2021, Silva, A. and Leino, K.R.M., Eds., Lecture Notes in Computer Science, vol. 12760, Springer, 2021, pp. 911–935. https://doi.org/10.1007/978-3-030-81688-9_42CrossRefMATH

37.

Tuerk, T., Local reasoning about while-loops, Proc. Theory Workshop at VSTTE 2010, 2010, pp. 29–39.

38.

Blanchard, A., Loulergue, F., and Kosmatov, N., Towards full proof automation in Frama-C using auto-active verification, NASA Formal Methods. NFM 2019, Badger, J. and Rozier, K., Eds., Lecture Notes in Computer Science, vol. 11460, Springer, 2019, pp. 88–105. https://doi.org/10.1007/978-3-030-20652-9_6CrossRef

39.

Baudin, P., Bobot, F., Bühler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., and Williams, N., The dogged pursuit of bug-free C programs: the Frama-C software analysis platform, Commun. ACM, 2021, vol. 64, no. 8, pp. 56–68. https://doi.org/10.1145/3470569CrossRef

40.

Attali, I., Caromel, D., and Wendelborn, A., A formal semantics and an interactive environment for Sisal, Tools and Environments for Parallel and Distributed Systems, Zaky, A. and Lewis, T., Eds., The Springer International Series in Software Engineering, vol. 2, Boston, Springer, 1996, pp. 229–256. https://doi.org/10.1007/978-1-4615-4123-3_11

41.

Kondratyev, D. and Promsky, A., Proof strategy for automated Sisal program verification, Software Technology: Methods and Tools. TOOLS 2019, Mazzara, M., Bruel, JM., Meyer, B., and Petrenko, A., Eds., Lecture Notes in Computer Science, vol. 11771, Cham: Springer, 2019, pp. 113–120. https://doi.org/10.1007/978-3-030-29852-4_9CrossRef

42.

Beckert, B., Bingmann, T., Kiefer, M., Sanders, P., Ulbrich, M., and Weigl, A., Relational equivalence proofs between imperative and MapReduce algorithms, Verified Software. Theories, Tools, and Experiments. VSTTE 2018, Piskac, R. and Rümmer, P., Eds., Lecture Notes in Computer Science, vol. 11294, Springer, 2018, pp. 248–266. https://doi.org/10.1007/978-3-030-03592-1_14

43.

Parthasarathy, G., Müller, P., and Summers, A., Formally validating a practical verification condition generator, Computer Aided Verification. CAV 2021, Silva, A. and Leino, K.R.M., Eds., Lecture Notes in Computer Science, vol. 12760, Springer, 2021, pp. 704–727. https://doi.org/10.1007/978-3-030-81688-9_33CrossRef

Titel: Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System
verfasst von: D. A. Kondratyev
Publikationsdatum: 01.12.2022
Verlag: Pleiades Publishing
Erschienen in: Automatic Control and Computer Sciences / Ausgabe 7/2022
Print ISSN: 0146-4116
Elektronische ISSN: 1558-108X
DOI: https://doi.org/10.3103/S0146411622070070

Neuer Inhalt

Bildnachweise

VDI-Icon, Profil Icon, inhalt2, Springer Professional Modul/© Springer Fachmedien Wiesbaden GmbH, Internationaler Motorenkongress/© [M] ATZlive | Chisnikov / Fotolia.com, Search Icon, Banner Hanser, Gamification/© Sergey Shulgin / Getty Images / iStock, Benedikt Bonnmann von Adesso/© Adesso, Teilzeit/© Fokussiert / stock.adobe.com, Zeitschrift Wissensmanagement Cover, PatentFit-Logo/© Springer Fachmedien Wiesbaden GmbH, 2023_Antrieb/© supervisuell, ATZ-Webinar: Prototypenfreie Entwicklung durch Offline- und Driver-in-the-Loop-HiL-Tests /© (c) VI-grade, chassis.tech plus 2023/© [M] ATZlive / TÜV SÜD PRODUCT SERVICE GMBH

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Weitere Artikel der Ausgabe 7/2022

NP-Completeness of the Minimum Spanning Tree Problem of a Multiple Graph of Multiplicity k ≥ 3

An Algorithm for Estimating the Signal Frequency at the Output of a Channel with a Controlled Information Flow under Phase Noise

Computational Analysis of Quantitative Characteristics of Some Residual Properties of Solvable Baumslag–Solitar Groups

LTL-Specification of Counter Machines

Satisfiability and Model Checking for One Parameterized Extension of Linear Temporal Logic

Erratum to: On the Detection of Exploitation of Vulnerabilities That Leads to the Execution of a Malicious Code

Neuer Inhalt

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.