Formal Methods: From Academia to Industrial Practice. A Travel Guide

• URL: http://arxiv.org/abs/2002.07279v3
• Date: Tue, 13 Feb 2024 03:11:38 GMT
• Title: Formal Methods: From Academia to Industrial Practice. A Travel Guide
• Abstract summary: No real change in industrial software development seems to be occurring. Gap between what formal methods can achieve and the daily software-development practice does not appear to be getting smaller.
• Score: 46.04829474801786
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: For many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief and many individual success stories, no real change in industrial software development seems to be occurring. In fact, the software industry itself is moving forward rapidly, and the gap between what formal methods can achieve and the daily software-development practice does not appear to be getting smaller (and might even be growing). In the past, many recommendations have already been made on how to develop formal-methods research in order to close this gap. This paper investigates why the gap nevertheless still exists and provides its own recommendations on what can be done by the formal-methods-research community to bridge it. Our recommendations do not focus on open research questions. In fact, formal-methods tools and techniques are already of high quality and can address many non-trivial problems; we do give some technical recommendations on how tools and techniques can be made more accessible. To a greater extent, we focus on the human aspect: how to achieve impact, how to change the way of thinking of the various stakeholders about this issue, and in particular, as a research community, how to alter our behaviour, and instead of competing, collaborate to address this issue.

Related papers

• The FIL Hypothesis: Inductive Biases Help with Kernel Engineering [88.25617363280156]
  General-purpose methods that scale with computation and data ultimately outperform those with built-in human knowledge.<n>We revisit this principle by observing a new and critical scaling dimension: the duration of the Feedback Information Loop (FIL)<n>We argue that future AI applications in science and the physical world will inherently involve FILs ranging from hours to weeks.
  arXiv  Detail & Related papers  (2026-06-29T15:16:33Z)
• Guidelines to Prompt Large Language Models for Code Generation: An Empirical Characterization [82.29178197694819]
  We derive and evaluate development-specific prompt optimization guidelines.<n>We use an iterative, test-driven approach to automatically refine code generation prompts.<n>We conduct an assessment with 50 practitioners, who report their usage of the elicited prompt improvement patterns.
  arXiv  Detail & Related papers  (2026-01-19T15:01:42Z)
• Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report) [5.130336628792388]
  We discuss our experiences with identifying and applying formal methods tools on an electronic warfare (EW) system with stringent safety requirements.<n>We present suggestions for improving formal methods usability including better documentation of capabilities, decreased manual effort, and improved handling of library code.
  arXiv  Detail & Related papers  (2026-01-16T18:46:19Z)
• The Prompt Engineering Report Distilled: Quick Start Guide for Life Sciences [0.016851255229980582]
  This report focuses on 6 core prompt techniques: zero-shot, few-shot approaches, thought generation, ensembling, self-criticism, and decomposition.<n>We provide detailed recommendations for how prompts should and shouldn't be structured.<n>We examine the effectiveness of Deep Research tools across OpenAI, Google, Anthropic and Perplexity platforms.
  arXiv  Detail & Related papers  (2025-09-14T14:39:35Z)
• No Regrets: Investigating and Improving Regret Approximations for Curriculum Discovery [53.08822154199948]
  Unsupervised Environment Design (UED) methods have gained recent attention as their adaptive curricula promise to enable agents to be robust to in- and out-of-distribution tasks. This work investigates how existing UED methods select training environments, focusing on task prioritisation metrics. We develop a method that directly trains on scenarios with high learnability.
  arXiv  Detail & Related papers  (2024-08-27T14:31:54Z)
• A Survey on Model MoErging: Recycling and Routing Among Specialized Experts for Collaborative Learning [136.89318317245855]
  MoErging aims to recycle expert models to create an aggregate system with improved performance or generalization. A key component of MoErging methods is the creation of a router that decides which expert model(s) to use for a particular input or application. This survey includes a novel taxonomy for cataloging key design choices and clarifying suitable applications for each method.
  arXiv  Detail & Related papers  (2024-08-13T17:49:00Z)
• Effective Technical Reviews [0.7212939068975619]
  While executing a program is the ultimate test for its correctness reviewing the program can occur earlier in its development and find problems if done effectively. This work focuses on review techniques. It enables the programmer to effectively review a program and find a range of problems from to interface issues.
  arXiv  Detail & Related papers  (2024-07-02T15:19:52Z)
• How are We Detecting Inconsistent Method Names? An Empirical Study from Code Review Perspective [13.585460827586926]
  Proper naming of methods can make program code easier to understand, and thus enhance software maintainability. Much research effort has been invested into building automatic tools that can check for method name inconsistency. We present an empirical study on how state-of-the-art techniques perform in detecting or recommending consistent and inconsistent method names.
  arXiv  Detail & Related papers  (2023-08-24T10:39:18Z)
• Practical Bandits: An Industry Perspective [7.682671667564167]
  The bandit paradigm provides a unified modeling framework for problems that require decision-making under uncertainty. With the bandit lens comes the promise of direct optimisation for the metrics we care about. This tutorial will take a step towards filling that gap between the theory and practice of bandits.
  arXiv  Detail & Related papers  (2023-02-02T17:03:40Z)
• 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)
• A Manifesto for Applicable Formal Methods [0.0]
  Our hypothesis is that formal methods still seem not to be applicable enough or ready for their intended use. This manifesto strives to foster an increased use of formal methods to the maximum benefit.
  arXiv  Detail & Related papers  (2021-12-23T18:24:28Z)
• A Review of Uncertainty Quantification in Deep Learning: Techniques, Applications and Challenges [76.20963684020145]
  Uncertainty quantification (UQ) plays a pivotal role in reduction of uncertainties during both optimization and decision making processes. Bizarre approximation and ensemble learning techniques are two most widely-used UQ methods in the literature. This study reviews recent advances in UQ methods used in deep learning and investigates the application of these methods in reinforcement learning.
  arXiv  Detail & Related papers  (2020-11-12T06:41:05Z)
• A Methodology for Creating AI FactSheets [67.65802440158753]
  This paper describes a methodology for creating the form of AI documentation we call FactSheets. Within each step of the methodology, we describe the issues to consider and the questions to explore. This methodology will accelerate the broader adoption of transparent AI documentation.
  arXiv  Detail & Related papers  (2020-06-24T15:08:59Z)

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.