Synthesizing Probabilistic Invariants via Doob's Decomposition

CAV, 2016.

Cited by: 24|Bibtex|Views9|Links
EI

Abstract:

When analyzing probabilistic computations, a powerful approach is to first find a martingale—an expression on the program variables whose expectation remains invariant—and then apply the optional stopping theorem in order to infer properties at termination time. One of the main challenges, then, is to systematically find martingales.

Code:

Data:

Your rating :
0

 

Tags
Comments