Wilkerson claimed the CQual++ tool found hundreds of bugs in Debian with a 50% positive rate. Said it also spotted Heartbleed. Worth independent testing on some known-buggy code or projects with little attention to see what it can do.
Liquid Types is another interesting one more people need to try out on various types of code to assess effectiveness & ease of use:
I'm wondering to what extent that this kind of Dataflow Analysis can be used in scripting languages such as Python or MUMPS. Deciding properties over all elements of an array is difficult, just as checking every element is time consuming. There is also some concern re proper treatment of sparse arrays when doing matrix calculations.
In principle this is possible, but given the complex semantics of language terms, this will be quite complex. Typically DFA is run on intermediate code in the optimising part of a compiler. Intermediate code is typically RISC-like idealised machine code. Each specific instruction is very simple and hence computing its effect on global data flow can easily be worked out.
http://dsw.users.sonic.net/oink/
Wilkerson claimed the CQual++ tool found hundreds of bugs in Debian with a 50% positive rate. Said it also spotted Heartbleed. Worth independent testing on some known-buggy code or projects with little attention to see what it can do.
Liquid Types is another interesting one more people need to try out on various types of code to assess effectiveness & ease of use:
http://goto.ucsd.edu/csolve/