We apply multivariate Lagrange interpolation to synthesizing polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of a 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.
CITATION STYLE
Chen, Y. F., Hong, C. D., Wang, B. Y., & Lijun, Z. (2015). Counterexample-guided polynomial loop invariant generation by lagrange interpolation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9206, pp. 658–674). Springer Verlag. https://doi.org/10.1007/978-3-319-21690-4_44
Mendeley helps you to discover research relevant for your work.