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
- Authors: Marieke Huisman, Dilian Gurov, and Alexander Malkis
- 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
- 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.