Automated Reasoning in Systems Engineering
- Laura Kovacs, Professor in Computer Science at the TU Wien
KAUST
In this talk I will present recent advancement in automated reasoning, in particular computer-supported theorem proving, for generating and proving software properties that prevent programmers from introducing errors while making changes in this software. When testing programs manipulating the computer memory, our initial results show our work is able to prove that over 80% of test cases are guaranteed to have the expected behavior.
Overview
Abstract
In this talk I will present recent advancement in automated reasoning, in particular computer-supported theorem proving, for generating and proving software properties that prevent programmers from introducing errors while making changes in this software. When testing programs manipulating the computer memory, our initial results show our work is able to prove that over 80% of test cases are guaranteed to have the expected behavior.
The work described in this talk, and its results, are supported by an ERC Starting Grant and ERC Proof of Concept Grant, aiming at providing ICT customers and investors a tool-supported methodology for ensuring continuous growth in software functionality, thus increasing software reliability and user's trust in software technologies.
Brief Biography
Laura Kovacs is full professor in computer science at the TU Wien, leading the automated program reasoning (APRe) group of the Formal Methods in Systems Engineering Division of the TU Wien.
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 work has been also awarded with an ERC Starting Grant 2014, an ERC Proof of Concept Grant 2018 and an ERC Consolidator Grant 2020.
