Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:backward_vcg_with_loops [2009/03/11 10:58]
vkuncak
sav08:backward_vcg_with_loops [2009/03/12 13:04] (current)
vkuncak
Line 45: Line 45:
  
 Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. ​ This can make loop invariant shorter. Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. ​ This can make loop invariant shorter.
- 
- 
  
 ===== Avoiding Exponential Explosion ===== ===== Avoiding Exponential Explosion =====
Line 55: Line 53:
   * [[http://​research.microsoft.com/​~leino/​papers/​krml157.pdf|Weakest preconditions for unstructured programs]]   * [[http://​research.microsoft.com/​~leino/​papers/​krml157.pdf|Weakest preconditions for unstructured programs]]
   * [[http://​citeseer.ist.psu.edu/​697165.html|Efficient weakest preconditions]]   * [[http://​citeseer.ist.psu.edu/​697165.html|Efficient weakest preconditions]]
 +
 +===== Encoding Interactive Proof Commands into Programs =====
 +
 +  * [[http://​lara.epfl.ch/​~kuncak/​papers/​ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Full Functional Verification of Linked Data Structures]]
  
 
sav08/backward_vcg_with_loops.txt · Last modified: 2009/03/12 13:04 by vkuncak
 
© EPFL 2018 - Legal notice