Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation

2015/02/15 by Yu‐Fang Chen, Chih-Duo Hong, Chen, Yu-Fang +5 · 2 citations
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Numerical Methods and Algorithms #Software Engineering (cs.SE)

paper · pdf · doi:10.48550/arxiv.1502.04280

openalex publication_date 2015/02/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Semantics of probabilistic programs

Cited by

• A Fresh Look at Best Inductive Loop Invariant Synthesis for Bit-Vector Relations
• Neuro-Symbolic Execution: The Feasibility of an Inductive Approach to Symbolic Execution

Related

• Finding polynomial loop invariants for probabilistic programs
• Generating Program Invariants via Interpolation
• Generating Loop Invariants by Computing Vanishing Ideals of Sample Points
• Automatically Generating Loop Invariants Using Quantifier Elimination
• MORA -- Automatic Generation of Moment-Based Invariants