Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Software is infrastructure: failures, successes, costs, and the case for formal verification

Giovanni Bernardi, Adrian Francalanza, Marco Peressotti, Mohammad Reza Mousavi

TL;DR

This chapter argues that software functions as critical infrastructure and that failures impose trillion-dollar costs. It champions formal verification and program analysis as principled approaches to prevent defects, supported by empirical data and industry case studies from healthcare, aerospace, rail, and IT. By detailing success stories, ROI, and educational strategies, it makes the case for investing in verification tools, methods, and curricula to reduce technical debt and improve safety. The work synthesizes historical failures with modern tooling (eg, TLA+, Frama-C, CompCert) to show practical paths toward scalable, trustworthy software systems. Its practical emphasis on governance, economics, and pedagogy aims to accelerate broad adoption of formal methods across domains.

Abstract

In this chapter we outline the role that software has in modern society, along with the staggering costs of poor software quality. To lay this bare, we recall the costs of some of the major software failures that happened during the last 40 years. We argue that these costs justify researching, studying and applying formal software verification and in particular program analysis. This position is supported by successful industrial experiences.

Software is infrastructure: failures, successes, costs, and the case for formal verification

TL;DR

This chapter argues that software functions as critical infrastructure and that failures impose trillion-dollar costs. It champions formal verification and program analysis as principled approaches to prevent defects, supported by empirical data and industry case studies from healthcare, aerospace, rail, and IT. By detailing success stories, ROI, and educational strategies, it makes the case for investing in verification tools, methods, and curricula to reduce technical debt and improve safety. The work synthesizes historical failures with modern tooling (eg, TLA+, Frama-C, CompCert) to show practical paths toward scalable, trustworthy software systems. Its practical emphasis on governance, economics, and pedagogy aims to accelerate broad adoption of formal methods across domains.

Abstract

In this chapter we outline the role that software has in modern society, along with the staggering costs of poor software quality. To lay this bare, we recall the costs of some of the major software failures that happened during the last 40 years. We argue that these costs justify researching, studying and applying formal software verification and in particular program analysis. This position is supported by successful industrial experiences.

Paper Structure

This paper contains 71 sections, 3 equations, 3 figures, 8 tables.

Table of Contents

  1. Introduction
  2. Software verification
  3. Formal methods
  4. Questions
  5. Empirical data
  6. Existing infrastructures
  7. Chips
  8. Datacenters
  9. DNS servers
  10. Healthcare
  11. Aggregated software cost
  12. The lack of quality is expensive
  13. Challenges for computer science students
  14. Concurrency
  15. The size of real-world programs
  16. ...and 56 more sections

Figures (3)

  • Figure 1: The Sleipner A Platform structural failure (cred. jakobsen1994sleipner).
  • Figure 2: The range gate is a specific segment of time during which the system anticipates receiving a reflection of a radar signal from a target based on the time it takes for a radar signal to travel to the target and return to the radar receiver. By calculating this round-trip time, the system can determine the distance to the target and predict where the target should be during the next radar scan. (Cred. gao1992patriot.)
  • Figure 3: A Venn diagram describing the relations between software validation, formal methods, and formal verification.