Counterexample-guided polynomial loop invariant generation by Lagrange interpolation

DOI10.1007/978-3-319-21690-4_44MaRDI QIDQ1702935zbMATH OpenOpenAlexFDO

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

Publication date 1 March 2018

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

Mathematics Subject Classification ID

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

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.

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

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)