I'm not entirely sure of the appropriate terminology here, so apologies if it's a bit vague.

Does Mathematica support symbolic analysis of computable functions? Can it determine whether any given computable function halts? (OK, just kidding.) For example, can it determine the statistical distribution of outcomes given an assumed distribution of inputs? The theory behind that one is in this paper: http://www.cs.sun.ac.za/~jaco/PAPERS/gdv12.pdf

I guess I'm wondering whether Mathematica can be used as an adjunct to existing static analysis tools that exist for various programming languages. If it could perform the probabilistic symbolic analysis described in the aforementioned paper, I would buy a copy straight away, so I'll make this into a feature request if the answer turns out to be no.

Thanks, cheers.

Jeremy