TY - GEN
T1 - Linear-invariant generation for probabilistic programs
T2 - 17th International Static Analysis Symposium, SAS 2010
AU - Katoen, Joost Pieter
AU - McIver, Annabelle K.
AU - Meinicke, Larissa A.
AU - Morgan, Carroll C.
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
KW - invariant generation
KW - Probabilistic programs
KW - quantitative program logic
KW - verification
UR - https://www.scopus.com/pages/publications/78149273666
U2 - 10.1007/978-3-642-15769-1_24
DO - 10.1007/978-3-642-15769-1_24
M3 - Conference proceeding contribution
AN - SCOPUS:78149273666
SN - 3642157688
SN - 9783642157684
VL - 6337 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 390
EP - 406
BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings
A2 - Cousot, Radhia
A2 - Martel, Matthieu
PB - Springer, Springer Nature
CY - Berlin
Y2 - 14 September 2010 through 16 September 2010
ER -