ProbTA: A sound and complete proof rule for probabilistic verification

TL;DR

This paper introduces ProbTA, a sound and complete proof rule for probabilistic program verification, enabling precise quantitative analysis through a novel modular approach and an automated CEGAR-based algorithm.

Contribution

It extends trace abstraction techniques to probabilistic programs with a new proof rule and automated algorithm, bridging verification and probability theory.

Findings

ProbTA provides sound and complete verification for probabilistic programs.

The approach enables precise quantitative analysis of violation probabilities.

An automated CEGAR-based algorithm is developed for practical verification.

Abstract

We propose a sound and complete proof rule ProbTA for quantitative analysis of violation probability of probabilistic programs. Our approach extends the technique of trace abstraction with probability in the control-flow randomness style, in contrast to previous work of combining trace abstraction and probabilisitic verification which adopts the data randomness style. In our method, a program specification is proved or disproved by decomposing the program into different modules of traces. Precise quantitative analysis is enabled by novel models proposed to bridge program verification and probability theory. Based on the proof rule, we propose a new automated algorithm via CEGAR involving multiple technical issues unprecedented in non-probabilistic trace abstraction and data randomness-based approach.