Abstract:
We describe applications of symbolic computation towards automating the formal analysis of while-programs implementing polynomial arithmetic.
We combine methods from static analysis, symbolic summation and computer algebra to derive polynomial loop invariants, yielding a finite representation of all polynomial equations that are valid before and after each loop execution. While deriving polynomial invariants is in general undecidable, we identify classes of loops for which we automatically can solve the problem of invariant synthesis.
We further generalize our work to the analysis of probabilistic program loops. Doing so, we compute higher-order statistical moments over (random) program variables, inferring this way quantitative invariants of probabilistic program loops. Our results yield computer-aided solutions in support of formal software verification, compiler optimization, and probabilistic reasoning.
Link to slides / materials here.
Short Bio:
Laura Kovacs is a full professor of 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, an ERC Consolidator Grant 2020, and Amazon Research Awards 2020 and 2023. Recently, she received financial support from LEA Frauenfonds to disseminate unplugged computer science to elementary schools, while organising computer science workshops with school children at the TU Wien.
