An assertion-based program logic for probabilistic programs

DOI10.1007/978-3-319-89884-1_5zbMATH Open1418.68049arXiv1803.05535OpenAlexW2962780947MaRDI QIDQ2323970FDOQ2323970

Authors: Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub 

Publication date: 13 September 2019

Abstract: Research on deductive verification of probabilistic programs has considered expectation-based logics, where pre- and post-conditions are real-valued functions on states, and assertion-based logics, where pre- and post-conditions are boolean predicates on state distributions. Both approaches have developed over nearly four decades, but they have different standings today. Expectation-based systems have managed to formalize many sophisticated case studies, while assertion-based systems today have more limited expressivity and have targeted simpler examples. We present Ellora, a sound and relatively complete assertion-based program logic, and demonstrate its expressivity by verifying several classical examples of randomized algorithms using an implementation in the EasyCrypt proof assistant. Ellora features new proof rules for loops and adversarial code, and supports richer assertions than existing program logics. We also show that Ellora allows convenient reasoning about complex probabilistic concepts by developing a new program logic for probabilistic independence and distribution law, and then smoothly embedding it into Ellora. Our work demonstrates that the assertion-based approach is not fundamentally limited and suggests that some notions are potentially easier to reason about in assertion-based systems.

Full work available at URL: https://arxiv.org/abs/1803.05535

Recommendations

• scientific article; zbMATH DE number 1500556
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• Reasoning about probabilistic sequential programs in a probabilistic logic
• Verification of Probabilistic Programs
• Validation of Stochastic Systems
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Program logic for higher-order probabilistic programs in Isabelle/HOL
• scientific article; zbMATH DE number 3890702
• Program verification as probabilistic inference

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cited In (8)

• Reasoning about probabilistic sequential programs
• Probabilistic Lipschitz analysis of neural networks
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• Credibilistic programming. An introduction to models and applications
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• VPHL: a verified partial-correctness logic for probabilistic programs
• Formal semantics of a classical-quantum language
• Title not available (Why is that?)

This page was built for publication: An assertion-based program logic for probabilistic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2323970)