LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
sav08:forward_symbolic_execution [2009/03/10 22:54]
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
Line 120: Line 120:
 Then we continue only from this one state. Then we continue only from this one state.
  
 +===== Execution =====
  
-===== Underapproximations =====+If the first statements are 
 +  assume (x=0) 
 +  assume (x=1) 
 +Then symbolic execution knows the exact values and can work as an interpreter.
  
-We next consider testing and debugging applications. 
  
-These can generate real counterexamples (underapproximation) ​as opposed to providing proofs (overapproximations).+===== Underapproximations ===== 
 + 
 +Here we generate real counterexamples (underapproximation), we compute smaller relation than one given by program semantics.
  
 If there are no loop invariants, we can still execute program on concrete inputs. ​ For symbolic initial state (e.g. giving upper bound of loop) execution need not terminate. If there are no loop invariants, we can still execute program on concrete inputs. ​ For symbolic initial state (e.g. giving upper bound of loop) execution need not terminate.
-  * Bounding depth: stop executing for path +  * Bounding depth: stop executing for paths longer than some value
   * Bounding state: small integer width, small number of objects in heap   * Bounding state: small integer width, small number of objects in heap
-  * Loop unrolling: replace loop( c ) with 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 =====
 +
 +In this case we compute overaproximation,​ bigger relation than the actual relation given by program semantics.
 +
 +Examples:
 +  * do not maintain exact expressions for variables, but only whether they are positive
 +  * 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
 +  * termination even for programs that have loops
 +  * useful information about the program (not exactly all information that we are interested in, depends on the approximation)
  
 ===== References ===== ===== References =====