Laura Kovacs(TU Wien)
hosted by Joël Ouaknine
"Algebra-based Analysis of Polynomial Probabilistic Programs"
We present fully automated approaches to safety and termination analysis of probabilistic while-programs whose guardsand expressions are polynomial expressions over random variables and parametrised distributions. We combine methods fromsymbolic summation and statistics to derive invariants as valid properties over higher-order moments, such as expectedvalues or variances, of program variables, synthesizing this way quantitative invariants of probabilistic program loops.We further extend our moments-based analysis to prove termination of considered probabilistic while-programs.This is a joint work with Ezio Bartocci, Joost-Pieter Katoen, Marcel Moosbrugger and Miroslav Stankovic.
Bio: Laura Kovacs is a full professor in computer science at the TU Wien, leading the automated program reasoning (APRe)group of the Formal Methods in Systems Engineering Division. Her research focuses on the design and development of newtheories, technologies, and tools for program analysis, with a particular focus on automated assertion generation,symbolic summation, computer algebra, and automated theorem proving. She is the co-developer of the Vampire theoremprover anda Wallenberg Academy Fellow of Sweden. Her research has also been awarded with a ERC Starting Grant 2014, an ERC Proofof Concept Grant 2018 and an ERC Consolidator Grant 2020.
|Time:||Wednesday, 22.09.2021, 10:00|