76 citations · 182 across the 15 of their papers we have counts for
3 papers · 1 filter
A New Proof Rule for Almost-Sure Termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski +1
An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be…
Abstract Hidden Markov Models: a monadic account of quantitative information flow
Annabelle McIver, Carroll Morgan, Tahiry Rabehaja
Hidden Markov Models, HMM's, are mathematical models of Markov processes with state that is hidden, but from which information can leak. They are typically represented as 3-way joi…
A new rule for almost-certain termination of probabilistic- and demonic programs
Annabelle McIver, Carroll Morgan
Extending our own and others' earlier approaches to reasoning about termination of probabilistic programs, we propose and prove a new rule for termination with probability one, als…