Differences

This shows you the differences between two versions of the page.

--- sav08:importance_of_verification [2010/01/25 11:49]
vkuncak
+++ sav08:importance_of_verification [2010/02/22 13:24]
vkuncak
@@ Line 1: / Line 1: @@
-====== Importance of Software Analysis and Verification ======
+====== Importance of Synthesis, Analysis and Verification ======
-===== Applications of Software Analysis and Verification =====
+===== Applications =====
-  * Reliability - higher assurance in program correctness by automated proofs (focus of this class)
+  * Reliability - higher assurance in program correctness by automated proofs
   * Programmer productivity - feedback on errors while typing program in e.g. Eclipse
       * [[http://snobol.cs.berkeley.edu/prospector/index.jsp|Prospector tool for finding code snippets]]
       * [[http://msevents.microsoft.com/CUI/WebCastEventDetails.aspx?culture=en-US&EventID=1032273351&CountryCode=US|Webcast of the Spec# programming system from Microsoft Research]], or just see [[http://lara.epfl.ch/~kuncak/lectures/SpecSharp.wmv|this file, minutes 12-23]]
+      * synthesis - large potential
   * Refactoring - check that suggested program transformations preserve program meaning
       * [[http://domino.research.ibm.com/comm/research_people.nsf/pages/tip.sas2007.html/$FILE/sas2007.pdf|Refactoring using Type Constraints]] by Frank Tip
@@ Line 26: / Line 27: @@
 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:
-  * [[http://sunnyday.mit.edu/papers/therac.ps|Between June 1985 and January 1987, six known accidents involved massive overdoses by the Therac-25 -- with resultant deaths and serious injuries]], see also [[{{sav08:radiation.pdf|recent NYT article}}
+  * [[http://sunnyday.mit.edu/papers/therac.ps|Between June 1985 and January 1987, six known accidents involved massive overdoses by the Therac-25 -- with resultant deaths and serious injuries]], see also {{sav08:radiation.pdf|recent NYT article}}
   * [[http://www.mailonsunday.co.uk/pages/live/articles/news/news.html?in_article_id=509289&amp;amp;in_page_id=1770|A kidney transplant patient was forced to have the new organ removed when it was discovered that the patient's blood type had been incorrectly recorded on a computer database]]
   * [[http://www.corpwatch.org/article.php?id=11110|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.''
@@ Line 111: / Line 112: @@
 {{sav08:harrison-slides.pdf|Theorem Proving for Verification}} slides of tutorial by [[http://www.cl.cam.ac.uk/~jrh|John Harrison]] in [[http://www.princeton.edu/cav2008/|CAV 2008]]