REVIEW 1 cited by
ProbTA: A sound and complete proof rule for probabilistic verification
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
ProbTA: A sound and complete proof rule for probabilistic verification
read the original 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.
Forward citations
Cited by 1 Pith paper
-
Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams
Typed extended decision diagrams enable scalable deductive verification of probabilistic programs by compactly representing weakest pre-expectations.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.