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.

@article{paperbot3734,
  title = {Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification},
  author = {Satoshi Kura and Hiroshi Unno and Takeshi Tsukada},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {PLDI},
  year = {2026},
  doi = {10.1145/3808348}
}