On lightweight Hoare logic of probabilistic programs: a bound tighter than the union bound
In the formal verification of probabilistic programming, lightweight Hoare logics are proposed to reason about a bound of the failure probability of non-probabilistic assertions. The existing lightweight Hoare logic, aHL, relies on the union bound, a tool from probabilistic theory. However, the union bound is loose in general.
In this work, we tighten the bound in aHL and prove its soundness and tightness. Downstream tools that rely on aHL can directly benefit from our out-of-the-box improvement. Practical applications to demonstrate the superiority of our theoretical improvements are in the plan.