Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

correctness_of_formula_propagation [2007/04/14 17:19]
vkuncak
correctness_of_formula_propagation [2007/04/15 18:40] (current)
vkuncak
Line 61: Line 61:
  
 With this transformation we can represent arbitrary control-flow graphs, and then we need to worry only about one loop.  Moreover, we can support control-flow constructs such as goto and break. With this transformation we can represent arbitrary control-flow graphs, and then we need to worry only about one loop.  Moreover, we can support control-flow constructs such as goto and break.
 +
 +**Note:** It does not matter how we obtained $\mbox{fact}_i(v)$ as long as, for the control flow graph $(V,E)$, we can find some values $\mbox{fact}(v)$ for each node $v \in V$, such that for each $(v,c,u) \in E$ we have
 +\begin{equation*}
 +  sp(\mbox{fact}(u),​c) \rightarrow \mbox{fact}(v)
 +\end{equation*}
 +
 +In particular, we could have guessed a loop invariant using some heuristics, or postupated invariant as a formula with some unknowns and then tried to solve for these unknowns.
 +
 
correctness_of_formula_propagation.txt · Last modified: 2007/04/15 18:40 by vkuncak