×

Counterexample-guided polynomial loop invariant generation by Lagrange interpolation. (English) Zbl 1381.68049

Kroening, Daniel (ed.) et al., Computer aided verification. 27th international conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015. Proceedings. Part I. Cham: Springer (ISBN 978-3-319-21689-8/pbk; 978-3-319-21690-4/ebook). Lecture Notes in Computer Science 9206, 658-674 (2015).
Summary: 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.
For the entire collection see [Zbl 1342.68028].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
41A05 Interpolation in approximation theory
PDFBibTeX XMLCite
Full Text: DOI arXiv