Software Verification

Not something we did formally in the enterprise, a couple of experiments with externally developed systems. but its high time it were included. 

Formal Software Verification Measures Up   By Samuel Greengard

Communications of the ACM, July 2021, Vol. 64 No. 7, Pages 13-15  10.1145/3464933

The modern world runs on software. From smartphones and automobiles to medical devices and power plants, executable code drives insight and automation. However, there is a catch: computer code often contains programming errors—some small, some large. These glitches can lead to unexpected results—and systematic failures.

"In many cases, software flaws don't make any difference. In other cases, they can cause massive problems," says Kathleen Fisher, professor and chair of the computer science department at Tufts University and a former official of the U.S. Defense Advanced Research Projects Agency (DARPA).

For decades, computer scientists have imagined a world where software code is formally verified using mathematical proofs. The result would be applications free from coding errors that introduce bugs, hacks, and attacks. Software verification would ratchet up device performance while improving cybersecurity and public safety. By applying specialized algorithms and toolkits, "It's possible to show that code completely meets predetermined specifications," says Bryan Parno, an associate professor in the computer science and electrical and computer engineering departments at Carnegie Mellon University.

At last, the technique is being used to verify the integrity of code in a growing array of real-world applications. The approach could fundamentally change computing. Yet, it is not without formidable obstacles, including formulating algorithms that can validate massive volumes of code at the speed necessary for today's world. The framework also suffers from the same problem every computing model does: if a verified proof is based on the wrong assumptions, it can validate invalid code and produce useless, and even dangerous, results.

"Formal verification is simply a way to up the ante," Fisher explains. "It's a way to modernize and improve the way software is written and ensure that it runs the way it is supposed to operate."  ... '