LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Last revision Both sides next revision
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   * 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://​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]]       * [[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   * 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       * [[http://​domino.research.ibm.com/​comm/​research_people.nsf/​pages/​tip.sas2007.html/​$FILE/​sas2007.pdf|Refactoring using Type Constraints]] by Frank Tip
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]] {{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]]
 +