--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Looking for paper describing Frama-C internals



Yes, these are the articles I was talking about. You could also look
at the documentation of CIL's generic dataflow analyses for
information (the value analysis uses the forward one).

On Thu, Sep 23, 2010 at 9:08 AM, David MENTRE <dmentre at linux-france.org> wrote:
> 2010/9/20 Pascal Cuoq <pascal.cuoq at gmail.com>:
>> B/ Dataflow algorithm
>>
>> 1/ without using option -slevel: basic dataflow propagation from
>> Kildall 73 / Cousot 77.
>
> Is it those articles?
>
> Patrick Cousot & Radhia Cousot.
> Abstract interpretation: a unified lattice model for static analysis
> of programs by construction or approximation of fixpoints.
> In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium
> on Principles of Programming Languages, pages 238?252, Los Angeles,
> California, 1977. ACM Press, New York.
> http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml
>
> A unified approach to global program optimization
> Annual Symposium on Principles of Programming Languages ?archive
> Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on
> Principles of programming languages table of contents
> Boston, Massachusetts
> Pages: 194 - 206
> Year of Publication: 1973
> Author
> Gary A. Kildall ? ? ? ? ?Naval Postgraduate School, Monterey, California
> http://portal.acm.org/citation.cfm?id=512927.512945&coll=GUIDE&dl=GUIDE&type=series&idx=SERIES317&part=series&WantType=Proceedings&title=POPL&CFID=105701026&CFTOKEN=43740434
>
> Sincerely yours,
> david
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>