Importance of Synthesis, Analysis and Verification
Applications
- Reliability - higher assurance in program correctness by automated proofs
- Programmer productivity - feedback on errors while typing program in e.g. Eclipse
- synthesis - large potential
- Refactoring - check that suggested program transformations preserve program meaning
- Refactoring using Type Constraints by Frank Tip
- Program optimizations - automatically transform program so that it takes less time, memory, power
- traditional application of program analysis:
- common subexpression elimination (F(e,e) –> let x = e in F(x,x))
- loop invariant hoisting: (while(p){x=e;c} –> x=e; while(p){c})
- strength reduction:
(for (i=0;i<M;i++) println(a[4*i]) --> (MM=4*M; for (j=0;j<MM;j+=4) println(a[j])))
- Data size optimizations for java programs by C. Scott Ananian, Martin C. Rinard
- Automatic parallelization of divide and conquer algorithms by Radu Rugina and Martin Rinard
Reliability: Software-Related Disasters
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:
- US: The Fatal Flaws in the Patriot Missile System by Jeffrey St. Clair, Counterpunch April 17th, 2003.
On March 24, a Patriot missile battery near the Kuwait border locked onto a British Royal Air Force Tornado G-4 jet that was returning from a raid on Basra. Four Patriot missiles were fired and one hit the jet, destroying the plane and killing two British pilots. Two days later, the radar for another Patriot missile battery locked on to a US F-16. The pilot of fighter jet located the radar dish and destroyed it. Then on April 2 an U.S. Navy F/A-18 Hornet was shot down by another Patriot missile, killing the pilot. “They're looking into a software problem,” said Navy Lt. Commander Charles Owens.
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
- Illustrative Risks by Peter G. Neumann, some of which are explained in more detail in Forum On Risks To The Public In Computers And Related Systems
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
- Modular checking for buffer overflows in the large Brian Hackett, Manuvir Das, Daniel Wang, Zhe Yang
- 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.
- 7 April 2005. AbsInt contributes to guaranteeing the safety of the A380, the world's largest passenger aircraft.
The Analyzer is able to verify the proper response time of the control software of all components by computing the worst-case execution time (WCET) of all tasks in the flight control software. This analysis is performed on the ground as a critical part of the safety certification of the aircraft.
Many success stories, but not as many as disasters
A lot of work remains.
Ongoing Initiatives
- Verified Software Repository, part of Grand Challenge on Verifying Compiler
- EPFL Center: http://tresor.epfl.ch
- upcoming projects
- COST Action on Verification of Object-Oriented Software: http://www.cost-ic0701.org/
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):
- A Basis for a Mathematical Theory of Computation by John McCarthy, 1961.
It is reasonable to hope that the relationship between computation and mathematical logic will be as fruitful in the next century as that between analysis and physics in the last. The development of this relationship demands a concern for both applications and for mathematical elegance. - Social processes and proofs of theorems and programs a controversial article by Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis
- Guarded Commands, Nondeterminacy and Formal Derivation of Programs by Edsger W. Dijkstra from 1975, and other Manuscripts
- Simple word problems in universal algebras by D. Knuth and P. Bendix (see Knuth-Bendix_completion_algorithm), used in automated reasoning
- Decidability of second-order theories and automata on infinite trees by Michael O. Rabin in 1965, proving decidability for one of the most expressive decidable logics
- Domains for Denotational Semantics by Dana Scott, 1982
- Assigning meanings to programs by R. W. Floyd, 1967
- The Ideal of Verified Software by C.A.R. Hoare
- Soundness and Completeness of an Axiom System for Program Verification by Stephen A. Cook
- An Axiomatic Definition of the Programming Language PASCAL by C. A. R. Hoare and Niklaus Wirth, 1973
- On the Computational Power of Pushdown Automata, by Alfred V. Aho, Jeffrey D. Ullman, John E. Hopcroft in 1970
- An Algorithm for Reduction of Operator Strength by John Cocke, Ken Kennedy in 1977
- A Metalanguage for Interactive Proof in LCF by Michael J. C. Gordon, Robin Milner, L. Morris, Malcolm C. Newey, Christopher P. Wadsworth, 1978
- Proof Rules for the Programming Language Euclid, by Ralph L. London, John V. Guttag, James J. Horning, Butler W. Lampson, James G. Mitchell, Gerald J. Popek, 1978
- Computational Complexity and Mathematical Proofs by J. Hartmanis
- Software reliability via run-time result-checking by Manuel Blum
- The Temporal Logic of Programs, by Amir Pnueli (see also the others of a few hundreds of publications)
- No Silver Bullet - Essence and Accidents of Software Engineering, by Frederick P. Brooks Jr., 1987
- Formal Development with ABEL, by Ole-Johan Dahl and Olaf Owe
- Abstraction Mechanisms in the Beta Programming Language, by Bent Bruun Kristensen, Ole Lehrmann Madsen, Birger Møller-Pedersen, Kristen Nygaard, 1983
- Formalization in program development, by Peter Naur, 1982
- Interprocedural Data Flow Analysis, by Frances E. Allen, 1974
- Counterexample-guided abstraction refinement for symbolic model checking by Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith, 2003
- Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications by Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla
- The Algorithmic Analysis of Hybrid Systems by Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine
The Role of Theorem Proving
Theorem Proving for Verification slides of tutorial by John Harrison in CAV 2008