Finding polynomial loop invariants for probabilistic programs

DOI10.1007/978-3-319-68167-2_26MaRDI QIDQ5096098zbMATH OpenOpenAlexFDO

Authors Yijun Feng, David N. Jansen, Naijun Zhan, Bican Xia, Lijun Zhang

Publication date 12 August 2022

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing polynomial invariants. In this paper, we propose an alternative approach. First, we fix a polynomial template as a candidate of a loop invariant. Using Stengle's Positivstellensatz and a transformation to a sum-of-squares problem, we find sufficient conditions on the coefficients. Then, we solve a semidefinite programming feasibility problem to synthesize the loop invariants. If the semidefinite program is unfeasible, we backtrack after increasing the degree of the template. Our approach is semi-complete in the sense that it will always lead us to a feasible solution if one exists and numerical errors are small. Experimental results show the efficiency of our approach.

Recommendations

• Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
• Synthesizing invariants by solving solvable loops
• Invariant generation for multi-path loops with polynomial assignments
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Synthesis for Polynomial Lasso Programs

Cited in

(10)

• Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
• Moment-based analysis of Bayesian network properties
• Reasoning about block-based cloud storage systems via separation logic
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Moment-based invariants for probabilistic loops with non-polynomial assignments
• Distribution estimation for probabilistic loops
• Data-Driven Invariant Learning for Probabilistic Programs
• Probabilistic program verification via inductive synthesis of inductive invariants
• Data-driven invariant learning for probabilistic programs
• Latticed \(k\)-induction with an application to probabilistic programs

This page was built for publication: Finding polynomial loop invariants for probabilistic programs

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