Reference:

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Apex: An analyzer for open probabilistic programs. In Madhusudan Parathasarathy and Sanjit A. Seshia, editors, Proceedings of the 24th International Conference on Computer Aided Verification (CAV), volume 7358 of LNCS, pages 693–698, Berkeley, California, USA, 2012. Springer.

Abstract:

We present APEX, a tool for analysing probabilistic programs that are open, i.e. where variables or even functions can be left unspecified. APEX transforms a program into an automaton that captures the program's probabilistic behaviour under all instantiations of the unspecified components. The translation is compositional and effectively leverages state reduction techniques. APEX can then further analyse the produced automata; in particular, it can check two automata for equivalence which translates to equivalence of the corresponding programs under all environments. In this way, APEX can verify a broad range of anonymity and termination properties of randomised protocols and other open programs, sometimes with an exponential speed-up over competing state-of-the-art approaches.

Suggested BibTeX entry:

@inproceedings{12KMOWW:CAV,
    address = {Berkeley, California, USA},
    author = {Stefan Kiefer and Andrzej S. Murawski and Jo\"el Ouaknine and Bj\"orn Wachter and James Worrell},
    booktitle = {Proceedings of the 24th International Conference on Computer Aided Verification (CAV)},
    editor = {Madhusudan Parathasarathy and Sanjit A. Seshia},
    pages = {693--698},
    publisher = {Springer},
    series = {LNCS},
    title = {APEX: An analyzer for open probabilistic programs},
    volume = {7358},
    year = {2012}
}