[cfe-dev] Extend Static Analyzer with Abstract Interpretation

[Ted Kremenek]

On Dec 13, 2012, at 6:07 AM, Bridge <bridge at iis.sinica.edu.tw> wrote:

> Thanks a lot for the advice, Anna and Ted.
> 
> I must agree that the core concept of the Analyzer is quite different from
> abstract interpretation, 
> 
> I've disucssed with my professors, and we will check if our idea can be
> modified to fit the Analyzer.
> 
> Hence, I would like to know if there are some documents describing
> theoretical basis of the project.
> 
> Also I found some papers below in the mentioned thread, but I'm not sure if
> they are outdated.
> 
> "Symbolic Path Simulation in PathSensitive Dataflow Analysis", and its
> previous work
> 
> "ESP: Path-sensitive program verification in polynomial time"
> 
> Thanks again for the help.

These papers are still relevant, although they there exact methodology is slightly different from what the analyzer does.  The idea of path-sensitive dataflow analysis is a fairly generic one, and it can be tackled with different specific techniques, but they all boil down to trying to compute a set of reachable program states.

Another good paper is:

  A System and Language for Building System-Specific, Static Analyses (Hallem et al)

and the more theoretical paper that talks about path-sensitive analysis as a graph reachability problem (not specific to finding bugs) is:

  Precise interprocedural dataflow analysis via graph reachability (Reps et al)

There are tons of other papers in this area, and the analyzer is inspired by many of them.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20121219/537878ed/attachment.html>