Linear-Invariant Generation for Probabilistic Programs:

DOI10.1007/978-3-642-15769-1_24zbMath1239.68020OpenAlexW1729037535WikidataQ57801444 ScholiaQ57801444MaRDI QIDQ4930741

Carroll Morgan, Larissa A. Meinicke, Annabelle McIver, Joost-Pieter Katoen

Publication date: 1 October 2010

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-15769-1_24

zbMATH Keywords

verificationinvariant generationprobabilistic programsquantitative program logic

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (12)

Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Understanding Probabilistic Programs ⋮ Approximate counting in SMT and value estimation for probabilistic programs ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Conditioning in probabilistic programming ⋮ Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops ⋮ On the hardness of analyzing probabilistic programs ⋮ Toward automatic verification of quantum programs ⋮ Probabilistic Lipschitz analysis of neural networks ⋮ Moment-based analysis of Bayesian network properties

Uses Software

• REDLOG

This page was built for publication: Linear-Invariant Generation for Probabilistic Programs: