76 citations · 182 across the 15 of their papers we have counts for
9 papers · 1 filter
Forward and Backward Simulations for Partially Observable Probability
Chris Chen, Annabelle McIver, Carroll Morgan
Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tracta…
Source-level reasoning for quantitative information flow
Chris Chen, Annabelle McIver, Carroll Morgan
We present a novel formal system for proving quantitative-leakage properties of programs. Based on a theory of Quantitative Information Flow (QIF) that models information leakage a…
Correctness by construction for probabilistic programs
Annabelle McIver, Carroll Morgan
The "correct by construction" paradigm is an important component of modern Formal Methods, and here we use the probabilistic Guarded-Command Language to illustrate…
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…
Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System
June Andronick, Corey Lewis, Carroll Morgan
We introduce a controlled concurrency framework, derived from the Owicki-Gries method, for describing a hardware interface in detail sufficient to support the modelling and verific…