  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.
