Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation
This work addresses the challenge of generating quantitative loop invariants for probabilistic programs, which is an incremental improvement in program verification methods.
The paper tackles the problem of synthesizing polynomial quantitative loop invariants for probabilistic programs by applying multivariate Lagrange interpolation to reduce unknown coefficients, with counterexample-guided refinement generating linear constraints to identify desired invariants. The authors evaluate their technique through several case studies with polynomial quantitative loop invariants in experiments.
We apply multivariate Lagrange interpolation to synthesize polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of an quantitative loop invariant to solving constraints over program variables and unknown coefficients. Lagrange interpolation allows us to find constraints with less unknown coefficients. Counterexample-guided refinement furthermore generates linear constraints that pinpoint the desired quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative loop invariants in the experiments.