On 4/9/07, <b class="gmail_sendername">Domagoj Babic</b> <<a href="mailto:babic.domagoj@gmail.com">babic.domagoj@gmail.com</a>> wrote:<div><span class="gmail_quote"></span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>Traditionally, such analyses have been considered too expensive to be<br>practical, and were mostly an academic curiosity. The core of the<br>problem is the lack of adequate automated decision procedures which<br>could quickly determine whether a set of constraints is satisfiable or
<br>not, and if it is satisfiable, find a solution.</blockquote><div><br>I think the real difficult thing in path sensitive program analysis (or symbolic execution)  is not the lack of decision procedures, but the translation of arbitrary pointer operations and library function calls in C/C++ program into the mathematics supported by the automated theorem prover.
<br>Almost every concept in the computer program except memory address has a counterpart in mathematics. I have tried to simulate memory by arrays in symbolic execution. But I found it is inadequate.<br></div><br></div><br>