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 new theories, 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 theorem prover and a Wallenberg Academy Fellow of Sweden. Her research has also been awarded with a ERC Starting Grant 2014, an ERC Proof of Concept Grant 2018 and an ERC Consolidator Grant 2020.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Saarbrücken

We present fully automated approaches to safety and termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions over random variables and parametrised distributions. We combine methods from symbolic summation and statistics to derive invariants as valid properties over higher-order moments, such as expected values 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.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

Annika Meiser

+49 681 9303 9105

--email hidden

public