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

TL;DR

This paper emphasizes the critical role of software in society, highlights the high costs of software failures, and advocates for formal verification methods supported by industrial successes.

Contribution

It advocates for formal software verification by illustrating its importance through failure costs and industrial case studies.

Findings

Major software failures have caused significant societal costs.

Formal verification has proven successful in industrial applications.

Investing in formal methods can reduce software failure costs.

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.