Lorenz Winkler

Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support

If all random samples have finite moments and the authors can verify a moment bound on the runtime of a linear loop, then they can automatically synthesise polynomial loop invariants that satisfy the OST and simplify the dui property to proving finiteness of the expected value of an expression depending on the update m...