Importance of Synthesis, Analysis and Verification


(for (i=0;i<M;i++) println(a[4*i]) --> (MM=4*M; for (j=0;j<MM;j+=4) println(a[j])))

Slides Illustrating Past Disasters

Software is used safety-critical systems (airplanes, cars, submarines). The consequences of errors are more severe than on desktops, so correctness standards must be higher. At the same time, complexity of systems bugs are more and more likely. In absence of automated tool support, disasters will happen. Here are examples of disasters:

Large commercial losses:

  • Pentium bugs encouraged hardware industry to embrace verification
  • Millions of bank accounts were impacted by errors due to installation of inadequately tested software code in the transaction processing system of a major North American bank, according to mid-2004 news reports. Articles about the incident stated that it took two weeks to fix all the resulting errors, that additional problems resulted when the incident drew a large number of e-mail phishing attacks against the bank's customers, and that the total cost of the incident could exceed $100 million.

For many more examples, see

Reliability: Some of the Success Stories

ASTREE Analyzer

“In Nov. 2003, ASTRÉE was able to prove completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and 50mn on a 64-bit AMD Athlon™ 64 using 580 Mb of memory).”

Interactive Theorem Provers

Some Commercial Tools

  • Coverity Prevent SAN FRANCISCO - January 8, 2008 - Coverity®, Inc., the leader in improving software quality and security, today announced that as a result of its contract with US Department of Homeland Security (DHS), potential security and quality defects in 11 popular open source software projects were identified and fixed. The 11 projects are Amanda, NTP, OpenPAM, OpenVPN, Overdose, Perl, PHP, Postfix, Python, Samba, and TCL.

Many success stories, but not as many as disasters

A lot of work remains.

Ongoing Initiatives

Impact on Computer Science

Here is the list of winners of the Turing award, ACM's most prestigious technical award. Here are some papers written by the award winners (not necessarily most representative of their work, but in some way connected to the topics of this class):

The Role of Theorem Proving