Lab for Automated Reasoning and Analysis 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
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