Data-driven invariant learning for probabilistic programs

DOI10.1007/S10703-024-00466-XMaRDI QIDQ6938563zbMATH OpenFDO

Authors Jialu Bao, Justin Hsu, Subhajit Roy

Publication date 25 August 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

probabilistic programsdata-driven invariant learningweakest pre-expectations

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)

Cites work

• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• scientific article; zbMATH DE number 3349291 (Why is no real title available?)
• A probabilistic PDL
• 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
• Probabilistic program verification via inductive synthesis of inductive invariants
• Semantics of probabilistic programs
• 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

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 Q6938563)