Eco-imp and Ev-imp
Eco-impperforms an expected cost analysis for simple imperative programs, in the style of Dijkstra's Guarded Command Language, featuring probabilistic sampling instructions, while ev-imp provides a fully automated expected value analysis of similar non-deterministic, probabilistic imperative programs.
However, in the presence of natural programming constructs such as procedures, local variables and recursion. Noteworthy, ev-imp is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights.
Contact
Ev-Imp is currently being further developed by the following developers