Counterexample-guided polynomial loop invariant generation by Lagrange interpolation

DOI10.1007/978-3-319-21690-4_44zbMATH Open1381.68049arXiv1502.04280OpenAlexW1948975400MaRDI QIDQ1702935FDOQ1702935

Authors: Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, Lijun Zhang 

Publication date: 1 March 2018

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1502.04280

Recommendations

• Finding polynomial loop invariants for probabilistic programs
• Invariant generation for multi-path loops with polynomial assignments
• Polynomial invariants by linear algebra
• Generating all polynomial invariants in simple loops
• Synthesis for Polynomial Lasso Programs

Mathematics Subject Classification ID

Interpolation in approximation theory (41A05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (6)

• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Static Analysis
• Finding polynomial loop invariants for probabilistic programs
• Moment-based analysis of Bayesian network properties
• Data-Driven Invariant Learning for Probabilistic Programs
• Probabilistic program verification via inductive synthesis of inductive invariants

This page was built for publication: Counterexample-guided polynomial loop invariant generation by Lagrange interpolation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1702935)