Lessons from Formally Verified Deployed Software Systems (Extended version)

• URL: http://arxiv.org/abs/2301.02206v3
• Date: Thu, 28 Mar 2024 22:01:48 GMT
• Title: Lessons from Formally Verified Deployed Software Systems (Extended version)
• Authors: Li Huang, Sophie Ebersold, Alexander Kogtenkov, Bertrand Meyer, Yinling Liu,
• Abstract summary: 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.
• Score: 65.69802414600832
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: The technology of formal software verification has made spectacular advances, but how much does it actually benefit the development of practical software? Considerable disagreement remains about the practicality of building systems with mechanically-checked proofs of correctness. Is this prospect confined to a few expensive, life-critical projects, or can the idea be applied to a wide segment of the software industry? To help answer this question, the present survey 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. Note: this version is the extended article, covering all the systems identified as relevant. A shorter version, covering only a selection, is also available.

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)
• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  We present the Code-Development Benchmark (Codev-Bench), a fine-grained, real-world, repository-level, and developer-centric evaluation framework. Codev-Agent is an agent-based system that automates repository crawling, constructs execution environments, extracts dynamic calling chains from existing unit tests, and generates new test samples to avoid data leakage.
  arXiv  Detail & Related papers  (2024-10-02T09:11:10Z)
• Estimating the Energy Footprint of Software Systems: a Primer [56.200335252600354]
  quantifying the energy footprint of a software system is one of the most basic activities. This document aims to be a starting point for researchers who want to begin conducting work in this area.
  arXiv  Detail & Related papers  (2024-07-16T11:21:30Z)
• Quantifying Software Correctness by Combining Architecture Modeling and Formal Program Analysis [41.375461087536294]
  QuAC is a modular approach for quantifying the correctness of service-oriented software systems. We present an implementation of QuAC for Java using the modeling tool Palladio and the deductive verification tool KeY.
  arXiv  Detail & Related papers  (2024-01-25T17:18:33Z)
• Charting a Path to Efficient Onboarding: The Role of Software Visualization [49.1574468325115]
  The present study aims to explore the familiarity of managers, leaders, and developers with software visualization tools. This approach incorporated quantitative and qualitative analyses of data collected from practitioners using questionnaires and semi-structured interviews.
  arXiv  Detail & Related papers  (2024-01-17T21:30:45Z)
• 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)
• End-of-Life of Software How is it Defined and Managed? [1.370633147306388]
  It is becoming quicker and cheaper to abandon old software and acquire new software that meets rapidly changing needs and demands. This paper will explore the systems engineering concept of end-of-life for software. It will bring forward examples of software that has been abandoned in an attempt to decommission and it will explore the repercussions of abandoned software artefacts.
  arXiv  Detail & Related papers  (2022-04-08T01:15:02Z)
• Empowered and Embedded: Ethics and Agile Processes [60.63670249088117]
  We argue that ethical considerations need to be embedded into the (agile) software development process. We put emphasis on the possibility to implement ethical deliberations in already existing and well established agile software development processes.
  arXiv  Detail & Related papers  (2021-07-15T11:14:03Z)
• A Review of Formal Methods applied to Machine Learning [0.6853165736531939]
  We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations.
  arXiv  Detail & Related papers  (2021-04-06T12:48:17Z)
• Machine Learning for Software Engineering: A Systematic Mapping [73.30245214374027]
  The software development industry is rapidly adopting machine learning for transitioning modern day software systems towards highly intelligent and self-learning systems. No comprehensive study exists that explores the current state-of-the-art on the adoption of machine learning across software engineering life cycle stages. This study introduces a machine learning for software engineering (MLSE) taxonomy classifying the state-of-the-art machine learning techniques according to their applicability to various software engineering life cycle stages.
  arXiv  Detail & Related papers  (2020-05-27T11:56:56Z)

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.