MOVES Seminar, 10 Sep 2009

 

Linear-invariant generation for probabilistic programs 

 

Larissa Meinicke (Macquarie Univ., Sydney)

 

 

Abstract: 

 

Automatic generation of invariants for qualitative programs has been a subject of research for over thirty years.  Relatively recent developments have shown that constraint-based methods are a suitable alternative to more traditional techniques, such as abstract interpretation. In this talk I discuss how constraint- based invariant-generation methods may be adapted to find quan- titative invariants for probabilistic programs. Quantitative invariants may be used to prove properties of probabilistic programs in the same way that their qualitative counterparts are used for qualitative program reasoning.