- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

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. | ||

+ |