VPHL: a verified partial-correctness logic for probabilistic programs

DOI10.1016/J.ENTCS.2015.12.021zbMath1351.68080OpenAlexW2220918360WikidataQ113317720 ScholiaQ113317720MaRDI QIDQ5971408

No author found.

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.021

zbMATH Keywords

formal verificationHoare logicprobabilistic programmingCoqnon-termination

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (3)

Markov chains and Markov decision processes in Isabelle/HOL ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving

Uses Software

• Unnamed Item
• EasyCrypt
• pGCL
• ALEA

Cites Work

• Proofs of randomized algorithms in Coq
• A probabilistic PDL
• Semantics of probabilistic programs
• Reasoning about probabilistic sequential programs
• Probabilistic guarded commands mechanized in HOL
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• Simple relational correctness proofs for static analyses and program transformations
• Reasoning About States of Probabilistic Sequential Programs
• Computer-Aided Security Proofs for the Working Cryptographer
• EasyCrypt: A Tutorial
• Formal certification of code-based cryptographic proofs
• Using Probabilistic Kleene Algebra for Protocol Verification
• An axiomatic basis for computer programming
• VPHL: a verified partial-correctness logic for probabilistic programs

This page was built for publication: VPHL: a verified partial-correctness logic for probabilistic programs