VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC

DOI10.1142/S012905410200114XzbMath1066.68081OpenAlexW2119029543WikidataQ129146979 ScholiaQ129146979MaRDI QIDQ3021957

E. P. de Vink, Jerry den Hartog

Publication date: 22 June 2005

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/s012905410200114x

zbMATH Keywords

probabilityrandomized algorithmsHoare logicprogram verificationprobabilistic predicates

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Randomized algorithms (68W20)

Related Items (13)

Formal semantics of a classical-quantum language ⋮ Reasoning about probabilistic sequential programs ⋮ A Systematic Approach to Probabilistic Pointer Analysis ⋮ Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs ⋮ VPHL: a verified partial-correctness logic for probabilistic programs ⋮ Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language ⋮ Toward automatic verification of quantum programs ⋮ Hoare Semigroups ⋮ Fifty years of Hoare's logic ⋮ A semantics and a logic for \textit{Fuzzy Arden Syntax} ⋮ On Probabilistic Techniques for Data Flow Analysis ⋮ Exogenous Probabilistic Computation Tree Logic ⋮ Generating functions for probabilistic programs

Cites Work

• A probabilistic PDL
• Bisimulation through probabilistic testing
• Probabilistic verification
• Reactive, generative, and stratified models of probabilistic processes
• Soundness and Completeness of an Axiom System for Program Verification
• An axiomatic basis for computer programming

This page was built for publication: VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC