Automatic probabilistic program verification through random variable abstraction

MaRDI QIDQ5151032zbMATH OpenFDO

Authors Damian Barsotti, Nicolás Wolovick

Publication date 16 February 2021

Full work available at URL http://eptcs.web.cse.unsw.edu.au/paper.cgi?QAPL2010.3

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Verification of Probabilistic Programs
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Abstraction Refinement for Probabilistic Software
• An abstract Monte-Carlo method for the analysis of probabilistic programs
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods

Cited in

(6)

• Abstraction Refinement for Probabilistic Software
• scientific article; zbMATH DE number 1953029 (Why is no real title available?)
• A weakest pre-expectation semantics for mixed-sign expectations
• Linear-invariant generation for probabilistic programs: automated support for proof-based methods
• Verification of Probabilistic Programs
• Data-Driven Invariant Learning for Probabilistic Programs

This page was built for publication: Automatic probabilistic program verification through random variable abstraction

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