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
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
 
© EPFL 2018 - Legal notice