Program verification as probabilistic inference

DOI10.1145/1190216.1190258MaRDI QIDQ3189808zbMATH OpenOpenAlexFDO

Authors Sumit Gulwani, Nebojsa Jojic

Publication date 12 September 2014

Published in Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1190216.1190258

zbMATH Keywords

automated recovery machinebelief networksfactor graphsforward and backward analysisGibbs samplinglearningMarkov chain Monte Carloover approximationprobabilistic inferenceprogram verificationunder approximation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Learning and adaptive systems in artificial intelligence (68T05) Randomized algorithms (68W20) Analysis of algorithms (68W40)

Recommendations

• Verification of Probabilistic Programs
• A provably correct sampler for probabilistic programs
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• Computer Aided Verification
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

Cited in

(12)

• Learning inductive invariants by sampling from frequency distributions
• An assertion-based program logic for probabilistic programs
• A modular static analysis approach to affine loop invariants detection
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• Combining model checking and data-flow analysis
• On the strength of “sometimes” and “always” in program verification
• scientific article; zbMATH DE number 1500556 (Why is no real title available?)
• From invariant checking to invariant inference using randomized search
• A provably correct sampler for probabilistic programs
• Computer Aided Verification
• Transformation-Enabled Precondition Inference
• Data-Driven Invariant Learning for Probabilistic Programs

This page was built for publication: Program verification as probabilistic inference

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