[cfe-dev] Static analysis tool development

Emmanuel Fleury fleury at labri.fr
Fri Jan 16 09:25:33 PST 2009


Hi all,

Monty Zukowski wrote:
> 
>>From the research I have done, clang seems to be the best front end
> for this type of project.  I have some questions:
> 
> 1) What is the state of the static analyzer?  Where do I start
> learning what needs done on it?  Is there a long term plan for it?

I would strongly suggest to start with:

Textbooks and introductory courses
==================================

- « Principles of Program Analysis » by Flemming Nielson, Hanne Riis
Nielson, Chris Hankin at Springer, 2005. ISBN 3-540-65410-0

- Introduction to Abstract Interpretation:
http://www.di.ens.fr/~cousot/aiintro.shtml
http://www.cs.mu.oz.au/~schachte/lpanalysis.html
http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/

- CEGAR and Lazy Abstraction
http://www.cs.cmu.edu/~emc/papers/Papers%20In%20Refereed%20Journals/Counterexample-guided%20abstraction%20refinement.pdf
http://mtc.epfl.ch/~tah/Publications/lazy_abstraction.pdf


Tools and Techniques
====================
- Astrée: http://www.astree.ens.fr/
See: http://www.di.ens.fr/~cousot/publications.www/Cousot-LNCS2000-lv-lb.pdf

- TVLA: http://www.cs.tau.ac.il/~tvla/
See: http://www.cs.tau.ac.il/~tvla/ifip2004.pdf

- Blast: http://mtc.epfl.ch/software-tools/blast/
See:
http://www.cs.sfu.ca/~dbeyer/Publications/2007-STTT.The_Software_Model_Checker_BLAST.pdf

- Slam: http://research.microsoft.com/en-us/projects/slam/
See: http://springerlink.metapress.com/content/ek3l4u815vl3aexk/

- The Magic tool: http://www.cs.cmu.edu/~chaki/magic/
See: http://www.cs.cmu.edu/~chaki/publications/TSE-2004.pdf

> 2) The ability to add custom logic to the analyzer is quite desirable.
>  Perhaps this could be made easier by integrating with a scripting
> language like Python.  To me, even the ability to write a script to
> pattern match against the AST or other intermediate forms could be
> quite useful.

Try to look at SMT solvers (see:
http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories).

MathSAT 4 seems to be quite efficient: http://mathsat4.disi.unitn.it/

Z3 is an attempt from Microsoft in this topic:
http://research.microsoft.com/en-us/um/redmond/projects/z3/


Hope this help !

Regards
-- 
Emmanuel Fleury

Associate Professor,         | Room:  261
LaBRI, Domaine Universitaire | Phone: +33 (0)5 40 00 69 34
351, Cours de la Libération  | Email: emmanuel.fleury at labri.fr
33405 Talence Cedex, France  | URL:   http://www.labri.fr/~fleury



More information about the cfe-dev mailing list