@inproceedings{bdb7290008a749d483b625c2f8069fc4,
title = "An Assertion-Based Logic for Local Reasoning about Probabilistic Programs",
abstract = "We introduce an assertion-based logic specifically designed for local reasoning about probabilistic programs featuring unbounded loops. Distribution formulas and their extensions facilitate the representation of invariants for unbounded loops in probabilistic programs. The assertions connected by separating conjunction exhibit probabilistic independence, which more intuitively displays the mutually independent properties of variables and ensures that the logic supports local reasoning. We prove the soundness of our logic and showcase its effectiveness through the formal verification of a wide range of examples including probabilistic inference in Bayesian networks and security analysis of cryptographic schemes.",
keywords = "Probabilistic programs, Separation logic, Local reasoning",
author = "Huiling Wu and Anran Cui and Yuxin Deng",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.; 10th International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2024 ; Conference date: 26-11-2024 Through 28-11-2024",
year = "2025",
doi = "10.1007/978-981-96-0602-3\_2",
language = "英语",
isbn = "9789819606016",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "25--45",
editor = "Timothy Bourke and Liqian Chen and Amir Goharshady",
booktitle = "Dependable Software Engineering. Theories, Tools, and Applications - 10th International Symposium, SETTA 2024, Proceedings",
address = "德国",
}