ERC Consolidator Grant 2020 ARTIST: Automated Reasoning with Theories and Induction for Software Technologies
PI Stories
10 marzo 2021
10 March 2021
share
Where: online on Zoom
Time: 1:30 pm
Second Seminar of the PI Stories
Speaker
- Laura Kovács, Vienna University of Technology
Abstract
The long list of software failures over the past years calls for serious concerns in our digital society, creating bad reputation and adding huge economic burden on organizations, industries and governments. Improving software reliability is no more enough, ensuring software reliability is mandatory. Our ARTIST project complements other advances in the area and addresses this demand by turning first-order theorem proving into an alternative, yet powerful approach to ensuring software reliability.
Saturation-based proof search is the leading technology for automated first-order theorem proving. The high-gain/high-risk aspect of our project comes from the development and use of saturation-based theorem proving as a unifying framework to reason about software technologies. We use first-order theorem proving methods not only to prove, but also to generate software properties that imply the absence of program errors at intermediate program steps.
Generating and proving program properties call for new methods supporting reasoning with both theories and quantifiers. Our project extends saturation-based first-order theorem provers with domain-specific inference rules to keep reasoning efficient. This includes commonly used theories in software development, such as the theories of integers, arrays and inductively defined data types, and automation of induction within saturation-based theorem proving, contributing to the ultimate goal of generating and proving inductive software properties, such as invariants.
Thanks to the full automation of our project, our results can be integrated and used in other frameworks, to allow end-users and developers of software technologies to gain from theorem proving without the need of becoming experts of it.
Registration
Free participation upon registration online by 8 March.
Register in advance for this meeting. After registering, you will receive a confirmation email containing information about joining the meeting.
Register in advance for this meeting. After registering, you will receive a confirmation email containing information about joining the meeting.
About the speaker
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 work has been also awarded with ERC Starting Grant 2014, an ERC Proof of Concept Grant 2018 and an ERC Consolidator Grant 2020.
Contact: iecs.school [at] unitn.it
PI Stories. A series of seminars aimed at providing the opportunity to the PhD students to learn the success stories of some of the most talented researchers in the world. Each speaker will present a research project he/she led as a principal investigator. The presentation will cover the scientific scope of the project and the most important results the project achieved. The speakers will also share their own experience of turning a research idea into a successful project winning a competitive grant.
Next story on 7 April 2021: Manuel Mazo Espinosa, Delft Center for Systems and Control -DCSC
Download
