Data-Driven Invariant Learning for Probabilistic Programs

DOI10.1007/978-3-031-13185-1_3MaRDI QIDQ6487311zbMATH OpenFDO

Authors Jialu Bao, Justin Hsu, Subhajit Roy

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-13185-1_3

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Linear-invariant generation for probabilistic programs: automated support for proof-based methods
• Verification of Probabilistic Programs
• Data-driven synthesis of full probabilistic programs
• Program verification as probabilistic inference
• Automatic probabilistic program verification through random variable abstraction

Cites work

• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• A probabilistic PDL
• A weakest pre-expectation semantics for mixed-sign expectations
• Abstraction, Refinement and Proof for Probabilistic Systems
• Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Counterexample-guided polynomial loop invariant generation by Lagrange interpolation
• Finding polynomial loop invariants for probabilistic programs
• Learning probabilistic termination proofs
• Semantics of probabilistic programs
• Symbolic model checking for probabilistic processes
• Synthesizing Probabilistic Invariants via Doob’s Decomposition
• Tail probabilities for randomized program runtimes via martingales for higher moments
• Termination analysis of probabilistic programs through Positivstellensatz's
• The Daikon system for dynamic detection of likely invariants
• Weakest precondition reasoning for expected run-times of probabilistic programs

Cited in

(8)

• Quantitative verification with neural networks
• Data-driven synthesis of full probabilistic programs
• Quantitative verification with neural networks
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
• Learning inductive invariants by sampling from frequency distributions
• Probabilistic program verification via inductive synthesis of inductive invariants
• Preface of the special issue on the conference on computer-aided verification 2022

This page was built for publication: Data-Driven Invariant Learning for Probabilistic Programs

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