<p>Don't worry too much about understanding everything in one source. Try reading several different articles and from their summaries and technical details, you may build up your own understanding.</p>

<ul>
<li><a href="http://srl.cs.berkeley.edu/~ksen/papers/cacm13.pdf">Symbolic Execution for Software Testing: Three Decades Later</a>, Cristian Cadar and Koushik Sen, 2013.</li>
<li><a href="http://www.ece.cmu.edu/~ejschwar/papers/oakland10.pdf">All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)</a>, Edward J. Schwartz, Thanassis Avgerinos, David Brumley, 2010.</li>
<li><a href="http://repository.cmu.edu/silicon_valley/53/">Symbolic Execution for Software Testing in Practice – Preliminary Assessment</a>, Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Pasareanu, Koushik Sen, Nikolai Tillmann, Willem Visser, 2011</li>
<li><a href="http://research.microsoft.com/en-us/um/people/pg/public_psfiles/laser2011.pdf">From Program to Logic: An Introduction</a>, Patrice Godefroid and Shuvendu Lahiri, 2012</li>
<li><a href="http://srl.cs.berkeley.edu/~ksen/concolic.html">Talk on concolic testing</a>, Koushik Sen</li>
<li><a href="http://fa11.pbworks.com/w/file/44841527/dart.pdf">Summary of DART</a>, Koushik Sen</li>
<li><a href="http://fa11.pbworks.com/w/file/44841523/cute.pdf">Summary of CUTE</a>, Koushik Sen</li>
<li><a href="http://channel9.msdn.com/blogs/peli/automated-whitebox-fuzz-testing-with-sage">Automated Whitebox Fuzz Testing with SAGE</a>, Patrice Godefroid</li>
<li><a href="http://fa09.pbworks.com/w/page/4233620/CUTE-Homework">A Lab exercise</a>, Koushik Sen</li>
</ul>

<p>If you are looking to develop your understanding by starting from a security context, I recommend this excellent summary of pointers to program analysis material from the <a href="http://www.reddit.com/r/ReverseEngineering/comments/smf4u/reverser_wanting_to_develop_mathematically/">Reverse Engineering reddit</a>. </p>

CC BY-SA 3.0
2013-07-06T07:51:02.930Z
2013-07-06T07:56:14.170Z
2013-07-06T07:56:14.170Z
Vijay D
<p>Being a beginner to Symbolic Execution (SE) myself, I would suggest:  </p>

<ul>
<li><a href="http://www.cs.uiuc.edu/class/sp11/cs477/king76symbolicexecution.pdf" rel="nofollow">Symbolic execution and program testing</a>: this is the paper to cite when you mention SE. It is easy to read, and provides the key idea without much logical formulation.  </li>
<li><a href="http://www.ece.cmu.edu/~ejschwar/papers/oakland10.pdf" rel="nofollow">All you ever wanted to know...</a>: this paper surveys SE and its applications to Security.  </li>
<li>The third step may be to learn an SE engine. I would suggest <a href="http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc" rel="nofollow">Symbolic Pathfinder</a>, it is open source and is actively maintained by NASA.  </li>
<li>Vijay mentioned CUTE, DART, SAGE but they are not traditional SE, they are <a href="http://en.wikipedia.org/wiki/Concolic_testing" rel="nofollow">concolic testing</a> tools, and are slightly different from SE described above. For example, for bounded programs, SE can be used as a verification tool, but concolic testing tools can not.  </li>
</ul>

<p>I hope this helps.</p>

CC BY-SA 3.0
2013-07-06T17:13:53.553Z
Thanks. I just finished reading the paper authored by J.King - [Symbolic execution and program testing](http://courses.engr.illinois.edu/cs477/sp2011/king76symbolicexecution.pdf). I spent a few hours on it and it truly was a remarkable way to get started.   I am looking forward to exploring other works. Also, I did realize that concolic execution differs from symbolic execution, but wasn't sure. Thank you for pointing out the difference.
dmkathayat
CC BY-SA 3.0
2013-07-07T00:47:40.313Z
The original King paper is very readable. Good suggestion! In current usage though, "symbolic execution" almost always refers to some derivative of symbolic execution and not strictly to King's original formulation. SE cannot be used even for bounded verification if there is no theorem prover support (for example, if expressions combine addition and multiplication, or arbitrary string or heap operations). This is one motivation for concolic methods.
Vijay D
CC BY-SA 3.0
2013-07-07T04:40:06.433Z
I agree with you. I do not mean SE is better than concolic testing, I just mean they are different. From Verification point of view: Verification > Symbolic Execution > Concolic Testing > Testing.
sean
CC BY-SA 3.0
2013-07-07T20:23:17.013Z
I think you should clarify what the ">" means. Also, this is an old view going back to Dijkstra and Hoare. I don't think people in the field hold that view anymore because there are tradeoffs on both side.
Vijay D
CC BY-SA 3.0
2013-07-06T16:46:40.870Z
2013-07-06T17:01:24.497Z
2013-07-06T17:01:24.497Z
sean
<p>I am an undergraduate CS student and currently reading on software security, particularly on static analysis of programs. I am particularly interested in understanding Symbolic Execution - an implementation technique under static analysis. </p>

<p>So far, I am unable to understand some of the research papers on the same, because of the lack of deep understanding of Symbolic Execution and its applications and uses.</p>

<p>There aren't many resources on the web, and the ones that are, assume a considerable formal knowledge on this domain from the reader beforehand.</p>

<p>I would appreciate if somebody can explain in depth the concept of Symbolic Execution and how it can be possibly used in program analysis - identifying bugs/vulnerabilities in softwares. 
Any links to some helpful resources on the same that would enable a security enthusiast to get started would be highly appreciated.</p>

CC BY-SA 3.0
2013-07-06T06:46:14.170Z
So you are looking for an accessible survey/lecture note/book on the topic of "Symbolic Execution"?
Kaveh
CC BY-SA 3.0
2013-07-06T06:54:54.520Z
@Kaveh: yes, that would be really helpful, especially if it is at a beginner-level, yet sophisticated enough for research paper survey.
dmkathayat
CC BY-SA 3.0
2013-07-06T07:53:28.143Z
Why do you say there are few resources? I have listed below only a few of those available and I wouldn't consider most of them heavy in formal details.
Vijay D
CC BY-SA 3.0
2013-07-06T07:55:52.963Z
@VijayD: Thanks for the links. Should help me get started.
dmkathayat
CC BY-SA 3.0
2013-07-07T09:06:47.800Z
@guerrero, I would recommend you to read the CACM 2013 article by Cadar and Sen to get an explanation of classic symbolic execution and the more modern counterpart and why it evolved in that direction.
Vijay D
CC BY-SA 3.0
2013-07-07T09:37:07.940Z
@VijayD: Indeed! I just finished reading that article: [Symbolic Execution for Software Testing: Three Decades Later](http://srl.cs.berkeley.edu/~ksen/papers/cacm13.pdf) and was about to comment here, until I saw yours. King's paper describes SE in its classical form as we call it today. Concolic execution is simply an extension of classical SE, providing mixed concrete and symbolic execution to overcome some significant limitations of its classical counterpart.
dmkathayat
CC BY-SA 3.0
2013-07-07T09:41:38.643Z
@VijayD: Also, I felt it is important to note that King's work was and remains tremendously ahead of its times, in a  theoretical sense, the only limitation being computation power, from which we suffer even today, hence the rise of modern symbolic execution techniques which tend to seek a workaround to achieve practicality using the present available computation powers. What do you opine?
dmkathayat
CC BY-SA 3.0
2013-07-07T20:22:02.057Z
@guerrero: Everyone acknowledges King and has done for a while, so he definitely gets credit. Limitation by computation power does not mean you are ahead of your times (else all brute force algorithms are ahead of the times). It's also limited by algorithms for reasoning about logics of data-types, which may not exist due to undecidability. The other problem is path explosion. The model checking and static analysis fields recognised these issues very early. (This site is not designed for discussion, so I do not recommend continuing it here)
Vijay D
CC BY-SA 3.0
2013-07-08T03:38:26.637Z
@VijayD: `Limitation by computation power does not mean you are ahead of your times`. That seems very valid. Thanks for your insights. And, recommendation accepted!
dmkathayat
<fl.formal-languages><formal-modeling><security><formal-methods><se.software-engineering>
Help in understanding Symbolic Execution
dmkathayat
# Help in understanding Symbolic Execution

(Asked by: username_0 on 2013-07-06)

I am an undergraduate CS student and currently reading on software security, particularly on static analysis of programs. I am particularly interested in understanding Symbolic Execution - an implementation technique under static analysis.

So far, I am unable to understand some of the research papers on the same, because of the lack of deep understanding of Symbolic Execution and its applications and uses.

There aren't many resources on the web, and the ones that are, assume a considerable formal knowledge on this domain from the reader beforehand.

I would appreciate if somebody can explain in depth the concept of Symbolic Execution and how it can be possibly used in program analysis - identifying bugs/vulnerabilities in softwares.
Any links to some helpful resources on the same that would enable a security enthusiast to get started would be highly appreciated.

**Tags:** fl.formal-languages, formal-modeling, security, formal-methods, se.software-engineering

> **Comments:**
> **username_1**: So you are looking for an accessible survey/lecture note/book on the topic of "Symbolic Execution"?  
> **username_0**: @username_1: yes, that would be really helpful, especially if it is at a beginner-level, yet sophisticated enough for research paper survey.  
> **username_2**: Why do you say there are few resources? I have listed below only a few of those available and I wouldn't consider most of them heavy in formal details.  
> **username_0**: @VijayD: Thanks for the links. Should help me get started.  
> **username_2**: @guerrero, I would recommend you to read the CACM 2013 article by Cadar and Sen to get an explanation of classic symbolic execution and the more modern counterpart and why it evolved in that direction.  
> **username_0**: @VijayD: Indeed! I just finished reading that article: [Symbolic Execution for Software Testing: Three Decades Later](http://srl.cs.berkeley.edu/~ksen/papers/cacm13.pdf) and was about to comment here, until I saw yours. King's paper describes SE in its classical form as we call it today. Concolic execution is simply an extension of classical SE, providing mixed concrete and symbolic execution to overcome some significant limitations of its classical counterpart.  
> **username_0**: @VijayD: Also, I felt it is important to note that King's work was and remains tremendously ahead of its times, in a  theoretical sense, the only limitation being computation power, from which we suffer even today, hence the rise of modern symbolic execution techniques which tend to seek a workaround to achieve practicality using the present available computation powers. What do you opine?  
> **username_2**: @guerrero: Everyone acknowledges King and has done for a while, so he definitely gets credit. Limitation by computation power does not mean you are ahead of your times (else all brute force algorithms are ahead of the times). It's also limited by algorithms for reasoning about logics of data-types, which may not exist due to undecidability. The other problem is path explosion. The model checking and static analysis fields recognised these issues very early. (This site is not designed for discussion, so I do not recommend continuing it here)  
> **username_0**: @VijayD: `Limitation by computation power does not mean you are ahead of your times`. That seems very valid. Thanks for your insights. And, recommendation accepted!  

---

## 2 answers

### Answer by username_2 on 2013-07-06. Score: 5

Don't worry too much about understanding everything in one source. Try reading several different articles and from their summaries and technical details, you may build up your own understanding.

* [Symbolic Execution for Software Testing: Three Decades Later](http://srl.cs.berkeley.edu/~ksen/papers/cacm13.pdf), Cristian Cadar and Koushik Sen, 2013.
* [All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)](http://www.ece.cmu.edu/~ejschwar/papers/oakland10.pdf), Edward J. Schwartz, Thanassis Avgerinos, David Brumley, 2010.
* [Symbolic Execution for Software Testing in Practice – Preliminary Assessment](http://repository.cmu.edu/silicon_valley/53/), Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Pasareanu, Koushik Sen, Nikolai Tillmann, Willem Visser, 2011
* [From Program to Logic: An Introduction](http://research.microsoft.com/en-us/um/people/pg/public_psfiles/laser2011.pdf), Patrice Godefroid and Shuvendu Lahiri, 2012
* [Talk on concolic testing](http://srl.cs.berkeley.edu/~ksen/concolic.html), Koushik Sen
* [Summary of DART](http://fa11.pbworks.com/w/file/44841527/dart.pdf), Koushik Sen
* [Summary of CUTE](http://fa11.pbworks.com/w/file/44841523/cute.pdf), Koushik Sen
* [Automated Whitebox Fuzz Testing with SAGE](http://channel9.msdn.com/blogs/peli/automated-whitebox-fuzz-testing-with-sage), Patrice Godefroid
* [A Lab exercise](http://fa09.pbworks.com/w/page/4233620/CUTE-Homework), Koushik Sen

If you are looking to develop your understanding by starting from a security context, I recommend this excellent summary of pointers to program analysis material from the [Reverse Engineering reddit](http://www.reddit.com/r/ReverseEngineering/comments/smf4u/reverser_wanting_to_develop_mathematically/).


---

### Answer by username_3 on 2013-07-06. Score: 1

Being a beginner to Symbolic Execution (SE) myself, I would suggest:

* [Symbolic execution and program testing](http://www.cs.uiuc.edu/class/sp11/cs477/king76symbolicexecution.pdf): this is the paper to cite when you mention SE. It is easy to read, and provides the key idea without much logical formulation.
* [All you ever wanted to know...](http://www.ece.cmu.edu/~ejschwar/papers/oakland10.pdf): this paper surveys SE and its applications to Security.
* The third step may be to learn an SE engine. I would suggest [Symbolic Pathfinder](http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc), it is open source and is actively maintained by NASA.
* Vijay mentioned CUTE, DART, SAGE but they are not traditional SE, they are [concolic testing](http://en.wikipedia.org/wiki/Concolic_testing) tools, and are slightly different from SE described above. For example, for bounded programs, SE can be used as a verification tool, but concolic testing tools can not.

I hope this helps.

> **Comments:**
> **username_0**: Thanks. I just finished reading the paper authored by J.King - [Symbolic execution and program testing](http://courses.engr.illinois.edu/cs477/sp2011/king76symbolicexecution.pdf). I spent a few hours on it and it truly was a remarkable way to get started.   I am looking forward to exploring other works. Also, I did realize that concolic execution differs from symbolic execution, but wasn't sure. Thank you for pointing out the difference.  
> **username_2**: The original King paper is very readable. Good suggestion! In current usage though, "symbolic execution" almost always refers to some derivative of symbolic execution and not strictly to King's original formulation. SE cannot be used even for bounded verification if there is no theorem prover support (for example, if expressions combine addition and multiplication, or arbitrary string or heap operations). This is one motivation for concolic methods.  
> **username_3**: I agree with you. I do not mean SE is better than concolic testing, I just mean they are different. From Verification point of view: Verification > Symbolic Execution > Concolic Testing > Testing.  
> **username_2**: I think you should clarify what the ">" means. Also, this is an old view going back to Dijkstra and Hoare. I don't think people in the field hold that view anymore because there are tradeoffs on both side.  

---

