Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
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