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:46] vkuncak |
sav08:forward_symbolic_execution [2009/03/11 10:47] vkuncak |
||
---|---|---|---|
Line 137: | Line 137: | ||
* Loop unrolling: replace loop( c ) with c[]c;c[]c;c;c for some number of times | * Loop unrolling: replace loop( c ) with c[]c;c[]c;c;c for some number of times | ||
* Instantiating values: find a satisfying assignment for R, take value v of x in it and replace e_x with v (moves towards concrete execution) | * Instantiating values: find a satisfying assignment for R, take value v of x in it and replace e_x with v (moves towards concrete execution) | ||
+ | |||
===== Overaproximation ===== | ===== Overaproximation ===== | ||
Line 146: | Line 147: | ||
* maintain only linear or certain polynomial constraints - if actual constraints are more complex, keep only the polynomial constraints that are guaranteed to hold | * maintain only linear or certain polynomial constraints - if actual constraints are more complex, keep only the polynomial constraints that are guaranteed to hold | ||
- | Why we approximate: we can obtain | + | Why we approximate we can obtain |
- | * termination | + | * termination even for programs that have loops |
- | * useful information (not exactly all information that we are interested in, depends on the approximation) | + | * useful information about the program (not exactly all information that we are interested in, depends on the approximation) |
===== References ===== | ===== References ===== |