We present a constraint-based method for automatically generating quantitative invariants for linear probabilistic programs, and we show how it can be used, in combination with proof-based methods, to verify properties of probabilistic programs that cannot be analysed using existing automated methods. To our knowledge, this is the first automated method proposed for quantitative-invariant generation. © 2010 Springer-Verlag.
CITATION STYLE
Katoen, J. P., McIver, A. K., Meinicke, L. A., & Morgan, C. C. (2010). Linear-invariant generation for probabilistic programs: Automated support for proof-based methods. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6337 LNCS, pp. 390–406). https://doi.org/10.1007/978-3-642-15769-1_24
Mendeley helps you to discover research relevant for your work.