[LLVMdev] New automated decision procedure for path-sensitive analysis

[Zhongxing Xu]

On 4/9/07, Domagoj Babic <babic.domagoj at gmail.com> wrote:
>
>
> Traditionally, such analyses have been considered too expensive to be
> practical, and were mostly an academic curiosity. The core of the
> problem is the lack of adequate automated decision procedures which
> could quickly determine whether a set of constraints is satisfiable or
> not, and if it is satisfiable, find a solution.


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.
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20070409/b49a306e/attachment.html>