Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Control flow graphs and code coverage

> I prefer to recommend you read some lecture notes or tutorial on static analysis.
> For example, the following is a quite good one
> http://www.itu.dk/people/brabrand/UFPE/Data-Flow-Analysis/static.pdf

Thanks for the link.

I hope to achieve a bit more progress by an other development approach.


> If you want to look at how its data structures and algorithms to implement it,
> you can read some chapters about lexing, parsing, abstract syntax tree,
> and data flow analysis in the “Modern compiler implementation” (in Java, C, or ML)
> book by Andrew Appel.

Another interesting information source …

How do much you influence various software by the reuse of function or class libraries
from the mentioned application domain?


> CTL and/or LTL are temporal logics which are used mostly in a verification technique
> called “Model Checking”.

Have you eventually looked at an approach which uses the technology "computation tree
logic with variables and witnesses" (CTL-VW) like it is described in the document
"A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking".
http://coccinelle.lip6.fr/papers/popl09.pdf
http://doi.acm.org/10.1145/1480881.1480897


Can your evolving software show any update suggestions which can be automatically
generated as patch files?

Regards,
Markus