Eco-imp and Ev-imp
Eco-imp führt eine Analyse der erwarteten Kosten für einfache imperative Programme im Stil von Dijkstras Guarded Command Language durch, die probabilistische Sampling-Anweisungen enthält, während ev-imp eine vollautomatische Erwartungswertanalyse ähnlicher nicht-deterministischer, probabilistischer imperativer Programme bietet.
Allerdings bei Vorhandensein von natürlichen Programmierkonstrukten wie Prozeduren, lokalen Variablen und Rekursion. Bemerkenswert ist, dass ev-imp nicht auf Tail-Rekursion beschränkt ist, die zweifelsohne durch Iteration ersetzt werden könnte und keine zusätzlichen Erkenntnisse erfordern würde.
Kontakt
Ev-Imp wird derzeit von den folgenden EntwicklerInnen weiterentwickelt