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
sav08:proving_correctness_of_some_small_examples [2010/02/22 12:13]
vkuncak
sav08:proving_correctness_of_some_small_examples [2015/04/21 17:30] (current)
Line 46: Line 46:
   * [[Notion of inductive loop invariant]]   * [[Notion of inductive loop invariant]]
   * What is and is not inductive loop invariant in this example   * What is and is not inductive loop invariant in this example
 +
 +A verification condition formula for preserving an invariant:
 +
 +++++|
 +\begin{equation*}
 +    r = i * x \land i=i+1 \land r' = r + x \rightarrow r' = i' * x
 +\end{equation*}
 +++++
 +  * we will see methods to prove such invariants
  
 === Transforming iterative version === === Transforming iterative version ===
Line 58: Line 67:
  
   * http://​javaverification.org/​   * http://​javaverification.org/​
 +
 +=== Another System ===
 +
   * [[http://​research.microsoft.com/​en-us/​projects/​vcc|VCC:​ A Verifier for Concurrent C]]   * [[http://​research.microsoft.com/​en-us/​projects/​vcc|VCC:​ A Verifier for Concurrent C]]