--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2016 ---
[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