Verification of Probabilistic Programs

DOI10.1137/0213021MaRDI QIDQ3316558zbMATH OpenOpenAlexFDO

Authors Amir Pnueli, Sergiu Hart, Micha Sharir

Publication date 1984

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/0213021

zbMATH Keywords

Markov chainsprogram verificationprobabilistic programs

Mathematics Subject Classification ID

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

Recommendations

• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Validation of Stochastic Systems
• scientific article; zbMATH DE number 1500556
• Automatic probabilistic program verification through random variable abstraction

Cited in

(37)

• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Probabilistic verification of Boolean functions
• Time-bounded termination analysis for probabilistic programs with delays
• Latticed \(k\)-induction with an application to probabilistic programs
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
• Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL
• A debugger for probabilistic programs
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods
• Probabilization of logics: completeness and decidability
• On the hardness of analyzing probabilistic programs
• Inter-program Properties
• Understanding probabilistic programs
• Decidability of finite probabilistic propositional dynamic logics
• Bounded model checking for probabilistic programs
• An assertion-based program logic for probabilistic programs
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• A generalisation of stationary distributions, and probabilistic program algebra
• scientific article; zbMATH DE number 2086517 (Why is no real title available?)
• Probabilistic verification and approximation
• Program verification as probabilistic inference
• Validation of Stochastic Systems
• On the complexity of deciding fair termination of probabilistic concurrent finite-state programs
• CONCUR 2005 – Concurrency Theory
• VPHL: a verified partial-correctness logic for probabilistic programs
• Does a Program Yield the Right Distribution?
• Verification of multiprocess probabilistic protocols
• Generating counterexamples for quantitative safety specifications in probabilistic B
• FM 2005: Formal Methods
• Constructive development of probabilistic programs
• Automatic probabilistic program verification through random variable abstraction
• Towards Automated Proof Support for Probabilistic Distributed Systems
• scientific article; zbMATH DE number 176732 (Why is no real title available?)
• Data-Driven Invariant Learning for Probabilistic Programs
• Probabilistic program verification via inductive synthesis of inductive invariants
• Proofs that count
• scientific article; zbMATH DE number 1500556 (Why is no real title available?)

This page was built for publication: Verification of Probabilistic Programs

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