Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:forward_symbolic_execution [2009/03/11 12:44]
philippe.suter
sav08:forward_symbolic_execution [2015/04/21 17:30] (current)
Line 18: Line 18:
  
 Maintain symbolic state formula $R(x_0,​y_0,​x,​y)$ in the following normal form: Maintain symbolic state formula $R(x_0,​y_0,​x,​y)$ in the following normal form:
-\[+\begin{equation*}
     x = e_x \land y = e_y \land P     x = e_x \land y = e_y \land P
-\]+\end{equation*}
 where $e_x$ is term describing symbolic state of $x$ and $e_y$ describes symbolic state of $y$.  The remaining part of the formula $R$ is given in //path condition// $P$.  It is a conjunction of all branch conditions up to current program point. ​ We require $P$ to be expressed only in terms of $x_0,y_0$, not $x,y$. where $e_x$ is term describing symbolic state of $x$ and $e_y$ describes symbolic state of $y$.  The remaining part of the formula $R$ is given in //path condition// $P$.  It is a conjunction of all branch conditions up to current program point. ​ We require $P$ to be expressed only in terms of $x_0,y_0$, not $x,y$.
  
Line 29: Line 29:
 ++++What should it do when encountering assert(F)? ++++What should it do when encountering assert(F)?
 |Generate proof obligation |Generate proof obligation
-\[+\begin{equation*}
     \forall x,y.\ ((\exists x_0,​y_0.R(x_0,​y_0,​x,​y)) \rightarrow F(x,y))     \forall x,y.\ ((\exists x_0,​y_0.R(x_0,​y_0,​x,​y)) \rightarrow F(x,y))
-\]+\end{equation*}
 that is, check the validity of $R \rightarrow F$. that is, check the validity of $R \rightarrow F$.
  
Line 56: Line 56:
  
 ++++How does this follow from relation composition?​| ++++How does this follow from relation composition?​|
-\[+\begin{equation*}
 \{((x0,​y0),​(x,​y)) \mid (x = e_x \land y = e_y \land P)\} \circ \{ ((x,​y),​(x',​y'​) \mid x' = f(x,y) \land y' = y \} \{((x0,​y0),​(x,​y)) \mid (x = e_x \land y = e_y \land P)\} \circ \{ ((x,​y),​(x',​y'​) \mid x' = f(x,y) \land y' = y \}
-\] +\end{equation*} 
-\[+\begin{equation*}
 \{((x0,​y0),​(x',​y'​)) \mid \exists x,y. (x = e_x \land y = e_y \land P \land x' = f(x,y) \land y' = y \} \{((x0,​y0),​(x',​y'​)) \mid \exists x,y. (x = e_x \land y = e_y \land P \land x' = f(x,y) \land y' = y \}
-\] +\end{equation*} 
-\[+\begin{equation*}
 \{((x0,​y0),​(x',​y'​)) \mid (x' = f(e_x,e_y) \land y' = e_y \land P \} \{((x0,​y0),​(x',​y'​)) \mid (x' = f(e_x,e_y) \land y' = e_y \land P \}
-\] +\end{equation*} 
-\[+\begin{equation*}
 \{((x0,​y0),​(x,​y)) \mid (x = f(e_x,e_y) \land y = e_y \land P \} \{((x0,​y0),​(x,​y)) \mid (x = f(e_x,e_y) \land y = e_y \land P \}
-\]+\end{equation*}
 ++++ ++++
  
Line 90: Line 90:
   assert(F(x,​y))   assert(F(x,​y))
 emit proof obligation: emit proof obligation:
-\[+\begin{equation*}
    (x = e_x \land y = e_y \land P) \rightarrow F(e_x,e_y)    (x = e_x \land y = e_y \land P) \rightarrow F(e_x,e_y)
-\]+\end{equation*}
 and change the state: and change the state:
   x := x_k (fresh)   x := x_k (fresh)
Line 154: Line 154:
 ===== References ===== ===== References =====
  
-  * [[http://​doi.acm.org/​10.1145/​360248.360252|Symbolic execution and program testing]] by James C. King+  * [[http://​doi.acm.org/​10.1145/​360248.360252|Symbolic execution and program testing]] by James C. King ({{sav08:​king76symbolicexecution.pdf|pdf}})
   * Lori Clarke and Debra Richardson: Symbolic Evaluation Methods for Program Analysis, in Program Flow Analysis: Theory and Applications,​ Prentice-Hall 1981.   * Lori Clarke and Debra Richardson: Symbolic Evaluation Methods for Program Analysis, in Program Flow Analysis: Theory and Applications,​ Prentice-Hall 1981.
   * [[http://​www.cs.utexas.edu/​users/​sandip/​publications/​symbolic-lpar/​main.html|Verification Condition Generation via Theorem Proving]]   * [[http://​www.cs.utexas.edu/​users/​sandip/​publications/​symbolic-lpar/​main.html|Verification Condition Generation via Theorem Proving]]
   * [[http://​osl.cs.uiuc.edu/​~ksen/​cute/​|CUTE Tool]]   * [[http://​osl.cs.uiuc.edu/​~ksen/​cute/​|CUTE Tool]]
 
sav08/forward_symbolic_execution.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice