Klever: Verification Framework for Critical Industrial C Programs

• URL: http://arxiv.org/abs/2309.16427v1
• Date: Thu, 28 Sep 2023 13:23:59 GMT
• Title: Klever: Verification Framework for Critical Industrial C Programs
• Authors: Ilja Zakharov, Evgeny Novikov, Ilya Shchepetkov
• Abstract summary: We present the Klever software verification framework, designed to reduce the effort of applying automatic software verification tools to large and critical industrial C programs. Existing tools do not provide widely adopted means for environment modeling, specification of requirements, verification of many versions and configurations of target programs, and expert assessment of verification results.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automatic software verification tools help to find hard-to-detect faults in programs checked against specified requirements non-interactively. Besides, they can prove program correctness formally under certain assumptions. These capabilities are vital for verification of critical industrial programs like operating system kernels and embedded software. However, such programs can contain hundreds or thousands of KLOC that prevent obtaining valuable verification results in any reasonable time when checking non-trivial requirements. Also, existing tools do not provide widely adopted means for environment modeling, specification of requirements, verification of many versions and configurations of target programs, and expert assessment of verification results. In this paper, we present the Klever software verification framework, designed to reduce the effort of applying automatic software verification tools to large and critical industrial C programs.

Related papers

• Enabling Unit Proofing for Software Implementation Verification [2.7325338323814328]
  We propose a research agenda for a unit proofing framework, both methods and tools. This will enable engineers to discover code-level defects early.
  arXiv  Detail & Related papers  (2024-10-18T18:37:36Z)
• The Impact of SBOM Generators on Vulnerability Assessment in Python: A Comparison and a Novel Approach [56.4040698609393]
  Software Bill of Materials (SBOM) has been promoted as a tool to increase transparency and verifiability in software composition. Current SBOM generation tools often suffer from inaccuracies in identifying components and dependencies. We propose PIP-sbom, a novel pip-inspired solution that addresses their shortcomings.
  arXiv  Detail & Related papers  (2024-09-10T10:12:37Z)
• Towards Quantifying Requirements Technical Debt for Software Requirements concerning Veracity: A Perspective and Research Roadmap [3.763215468259125]
  We present our perspective and the vision to apply the lens of RTD to software requirements concerning veracity. Our goal is to cultivate awareness of veracity as an important concern and eventually support the management of RTD for software requirements concerning veracity.
  arXiv  Detail & Related papers  (2024-06-29T10:10:03Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpec is an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It can be successfully applied to verify the programs in a real-world X509-parser project.
  arXiv  Detail & Related papers  (2024-03-31T18:15:49Z)
• Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
  We introduce Selene, which is the first project-level automated proof benchmark constructed based on the real-world industrial-level operating system microkernel, seL4. Our experimental results with advanced large language models (LLMs), such as GPT-3.5-turbo and GPT-4, highlight the capabilities of LLMs in the domain of automated proof generation.
  arXiv  Detail & Related papers  (2024-01-15T13:08:38Z)
• Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking [2.9129603096077332]
  We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. We have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker.
  arXiv  Detail & Related papers  (2023-11-09T11:25:24Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Using Machine Learning To Identify Software Weaknesses From Software Requirement Specifications [49.1574468325115]
  This research focuses on finding an efficient machine learning algorithm to identify software weaknesses from requirement specifications. Keywords extracted using latent semantic analysis help map the CWE categories to PROMISE_exp. Naive Bayes, support vector machine (SVM), decision trees, neural network, and convolutional neural network (CNN) algorithms were tested.
  arXiv  Detail & Related papers  (2023-08-10T13:19:10Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  In deductive verification and software model checking, dealing with certain specification language constructs can be problematic. We propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation.
  arXiv  Detail & Related papers  (2023-05-26T14:55:35Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  This article examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools.
  arXiv  Detail & Related papers  (2023-01-05T18:18:46Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  We propose fault-aware neural code rankers that can predict the correctness of a sampled program without executing it. Our fault-aware rankers can significantly increase the pass@1 accuracy of various code generation models.
  arXiv  Detail & Related papers  (2022-06-04T22:01:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.