Many quantitative properties of probabilistic programs can be characterized as least fixed points, but verifying their lower bounds remains a challenging problem.
We present a new approach to lower-bound verification that exploits and extends the connection between the uniqueness of fixed points and program termination.
The core technical tool is a generalization of ranking supermartingales, which serves as witnesses of the uniqueness of fixed points.
Our method provides a simple and unified reasoning principle applicable to a wide range of quantitative properties, including termination probability, the weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation.
We provide a template-based algorithm for automated verification of lower bounds and demonstrate the effectiveness of the proposed method via experiments.