Linear-invariant generation for probabilistic programs

Automated support for proof-based methods

Joost Pieter Katoen*, Annabelle K. McIver, Larissa A. Meinicke, Carroll C. Morgan

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

45 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationStatic Analysis - 17th International Symposium, SAS 2010, Proceedings
EditorsRadhia Cousot, Matthieu Martel
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Number of pages17
Volume6337 LNCS
ISBN (Print)3642157688, 9783642157684
Publication statusPublished - 2010
Event17th International Static Analysis Symposium, SAS 2010 - Perpignan, France
Duration: 14 Sep 201016 Sep 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6337 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349


Other17th International Static Analysis Symposium, SAS 2010


  • invariant generation
  • Probabilistic programs
  • quantitative program logic
  • verification

Fingerprint Dive into the research topics of 'Linear-invariant generation for probabilistic programs: Automated support for proof-based methods'. Together they form a unique fingerprint.

Cite this