Polynomial Quantitative Loop Invariants by Lagrange Interpolation
Abstract:
We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. Lagrange interpolation allows to find better constraints for unknown loop invariants. Random sampling furthermore generates constraints to pin- point quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative loop invariants in the experiments.