C Software Formal Verification
Keywords:
C software, formal verification, Artificial IntelligenceAbstract
This paper reviews briefly the literature on formal verification of C software. Most existing C software model checkers and automatic theorem provers deal well only with small size code C software. Furthermore, full mechanization of conventional techniques to reduce the verification process complexity as code summation and abstract interpretation is merely impossible. Another challenge is how to choose the most suitable tool(s) among a panoply of available tools. We think that Artificial Intelligence can mitigate the above problems. For instance, by applying machine learning algorithms, the verification tool can automatically infer properties to be checked and synthesize proofs.
References
J. Amilon, C. Lidström, and D. Gurov, “Deductive Verification Based Abstraction for Software Model Checking,” Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022.
M. Amrani, L. Lucio, and A. Bibal, “ML + FV = $heartsuit$? A Survey on the Application of Machine Learning to Formal Verification,” arXiv: Software Engineering, 2018.
T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani, “Automatic Predicate Abstraction of C Programs,” in PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pp. 203–213, 2001.
D. Beyer, “Competition on Software Verification and Witness Validation: SV-COMP 2023,” in: Sankaranarayanan, S., Sharygina, N. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. Lecture Notes in Computer Science, vol 13994, 2023.
F. Boutekkouk, “Towards Automatic Maude Specifications Generation From C Functions,” Journal of Innovation Information Technology and Application (JINITA), vol. 5(1), pp. 83–96, 2023.
P. Cousot, and R. Cousot, “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238—252, 1977.
P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-C A Software Analysis Perspective,” Formal Aspects of Computing, 2012.
E. W. Dijkstra, “A constructive approach to the problem of program correctness,” BIT Numerical Mathematics, vol. 8(3), pp.174-186, 1968.
E.W. Dijkstra, “Guarded commands, nondeterminacy and formal derivation of programs,” Commun. ACM, vol. 18, pp. 453–457, 1975.
C.M. Ellison, “A Formal Semantics of C with Applications,” PhD. thesis, University of Illinois, 2012.
J.-C. Filliatre, “Preuve de programmes impératifs en théorie des types,” Thèse de doctorat, Université Paris-Sud, 1999.
E. First and Y. Brun, “Diversity-Driven Automated Formal Verification,” 2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE), 2022.
R.W. Floyd, “Assigning meanings to programs,” Proceedings of the American Mathematical Society Symposia on Applied Mathematics, vol. 19, pp. 19–31, 1967.
J.A. Goguen and G. Malcolm, Algebraic Semantics of Imperative Programs (Book), MIT Press, ISBN: 9780262071727, 1996.
S. Hayashi, “Logic of refinement types,” in Proceedings of the Workshop on Types for Proofs and Programs, pp. 157–172, 1993.
W. A Howard, “The formulae-as-types notion of construction,” in Seldin, Jonathan P.; Hindley, J. Roger (eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 479–490, ISBN 978-0-12-349050-6, 1980.
C.A.R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol. 12(10), pp. 576–580, 1969.
F. Ivancic, I. Shlyakhter, A. Gupta, M.K. Ganai, V. Kahlon, C. Wang, and Z. Yang, “Model Checking C Programs Using F-SOFT,” International Conference on Computer Design 31 October, San Jose, CA, USA, 2005.
ISO/IEC 9899:2018, Information technology — Programming languages — C, https://www.iso.org/standard/74528.html
K. Jiang, “Model Checking C Programs by Translating C to Promela,” Master. thesis, Linkoping University, Sweden, 2009.
E. Kamburjan and N. Wasser, “The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics,” in 15th Interaction and Concurrency Experience (ICE 2022), EPTCS 365, pp. 1–16, 2022.
R. J. Krebbers, “The C standard formalized in Coq,” PhD. thesis, Radboud University Nijmegen, 2015.
J. Larkin and D. Justice, “Achieving the Quantum Advantage in Software,” Carnegie Mellon University, Software Engineering Institute's Insights (blog), Accessed November 8, 2023, https://insights.sei.cmu.edu/blog/achieving-the-quantum-advantage-in-software/.
N. Ge, M. Pantel, and X. Crégut, “Automated Failure Analysis in Model Checking based on Data Mining,” 4th International Conference On Model and Data Engineering, Larnaca, Cyprus, pp.13-28, ⟨10.1007/978-3-319-11587-0_4⟩. ⟨hal-03252269⟩, 2014.
M. Norrish, “C Formalised in HOL,” PhD. thesis, University of Cambridge, 1998.
S.H. Park, R. Pai, and T. Melham, “A Formal CHERI-C Semantics for Verification,” in: Sankaranarayanan, S., Sharygina, N. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. Lecture Notes in Computer Science, vol. 13993. Springer, Cham, 2023.
C. Pulte, D.C. Makwana, T. Sewell, K. Memarian, P. Sewell, and N. Krishnaswami, “CN: Verifying systems C code with separation-logic refinement types,” Proceedings of the ACM on Programming Languages, 7(POPL), pp.1-32, 2023.
J. C. Reynolds, “Separation Logic: A Logic for Shared Mutable Data Structures,” in Proceedings 17th Annual IEEE Symposium on Logic in Computer Science 22-25 July, 2022.
M. Richardson, “Why you should use standards-based development practices (even if you don’t have to),” https://www.embedded.com/ June 8, 2020.
M. Sammler, R. Lepigre, and R. Krebbers, “RefjnedC: Automating the Foundational Verifjcation of C Code with Refjned Ownership Types,” in PLDI ’21, Canada, 2021.
R. Sethi, “A Case Study in Specifying the Semantics of a Programming Language,” Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, pp.117–130, 1980.
T. Sharma, M. Kechagia, S. Georgiou, R. Tiwari, and F. Sarro, “A Survey on Machine Learning Techniques for Source Code Analysis,” ArXiv, abs/2110.09610, 2021.
N. Schirmer, “Verification of Sequential Imperative Programs in Isabelle/HOL,” PhD. thesis, Technische Universitat Munchen, 2005.
S. Sriya, L. Lavanya, M.M. Aditi, and N.S. Kumar, “Verification of C Programs using Annotations,” in 2019 IEEE Tenth International Conference on Technology for Education (T4E), Goa, India, 2019.
A. Stefanescu, “MatchC: A Matching Logic Reachability Verifier Using the K Framework,” in Electronic Notes in Theoretical Computer Science vol. 304, pp. 183–198, 2014.
H. Xi, “Dependent types in practical programming,” PhD. thesis, Department Computer Science, Carnegie-Mellon University, 1998.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2024 Fateh Boutekkouk
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
License Terms:
Except where otherwise noted, content on this website is lincesed under a Creative Commons Attribution Non-Commercial License (CC BY NC)
Use, distribution and reproduction in any medium, provided the original work is properly cited and is not used for commercial purposes, is permitted.
Copyright to any article published by WiPiEC retained by the author(s). Authors grant WiPiEC Journal a license to publish the article and identify itself as the original publisher. Authors also grant any third party the right to use the article freely as long as it is not used for commercial purposes and its original authors, citation details, and publisher are identified, in accordance with CC BY NC license. Fore more information on license terms, click here.