Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:forward_symbolic_execution [2009/03/11 10:47] vkuncak |
sav08:forward_symbolic_execution [2009/03/11 10:48] vkuncak |
||
|---|---|---|---|
| Line 17: | Line 17: | ||
| === Exploiting Analogy with Execution === | === Exploiting Analogy with Execution === | ||
| - | Maintain symbolic state formula $R(x_0,x)$ in the following normal form: | + | Maintain symbolic state formula $R(x_0,y_0,x,y)$ in the following normal form: |
| \[ | \[ | ||
| x = e_x \land y = e_y \land P | x = e_x \land y = e_y \land P | ||