Third ERC Grant for Laura Kovács

High-gain/high-risk project ARTIST aims to prevent software errors by turning the first-order theorem proving into an alternative, yet powerful approach to ensuring software reliability.

Software technologies are used everywhere, yet they are error-prone. The notorious example of Boeing Max 737 aeroplane crash from 2018/2019 reinforces the need for approaches and tools which can automatically determine the reliability of computer systems and software.

Laura Kovács (TU Wien) from the FORSYTE research group (Formal Methods in System Engineering) has received ERC Consolidator Grant 2020 from the European Research Council (ERC) for her project ARTIST – Automated Reasoning with Theories and Induction for Software Technology. Results of the project will be able to be easily integrated and used in other technologies, supporting end-users and developers of formal verification engines to apply saturation-based first order (FO) theorem proving without the need of becoming experts in FO reasoning. ARTIST project builds upon previous results from Laura Kovacs’s ERC projects, such as ERC Starting Grant and ERC Proof of Concept Grant. The methods and tools developed within the project will be evaluated on academic and industrial programs, in the framework of ongoing collaborations with verification teams at Microsoft Research, Amazon Web Services and Certora. The funding – up to €2 million per grant, plus in some cases an additional €1 million for start-up costs – is provided for up to five years and mostly covers the employment of researchers and other staff to consolidate the grantees’ teams.  

Automated reasoning and formal verification

The long list of software failures over the past years calls for a serious rethinking of the approaches improving software reliability. The area of formal methods, in particular automated reasoning and formal verification, addresses this demand, by providing rigorous mathematical arguments proving that the software has no errors. Yet, there are theoretical results showing that there is no “one” formal approach that can be used for every software error, in every technology.

Until recently, automated reasoning in formal verification was the sole domain of satisfiability modulo theory (SMT) solvers which are very powerful in dealing with quantifier-free formulas and arithmetic, but generally have very limited support for quantifiers. Formal verification however also requires reasoning about memory, heap, pointers, and unbounded data types such as arrays and inductively defined data types. Yet, the recent progress in automation for quantified reasoning in first-order (FO) theorem proving has not yet been fully integrated in formal verification.

Laura Kovács: “Our project enters new grounds and makes FO theorem proving an alternative, yet powerful approach to formal verification, complementing other advances in the area. We use FO theorem provers not only to prove but also to generate software properties, by developing novel reasoning techniques in the full FO theories of commonly used data structures of software technologies, including integers, arrays and inductively defined data types.”

ARTIST – Automated Reasoning with Theories and Induction for Software Technology

The timeliness of the project ARTIST is witnessed by the growing academic and industrial interest in automated reasoning. Microsoft is now routinely using SMT solving to formally verify network operations of its Azure cloud computing service. Automated reasoning is also one of the main investments made by AmazonWeb Services to ensure functional correctness and security of its products. The emergence of smart contracts has ignited several startups, including the Certora company which uses proving technologies to offer audits with rigorous guarantees. For many years now, according to the Open Web Application Security Project– OWASP, the highest-ranked security vulnerability comes from injection flaws, by “executing unintended commands or accessing data without proper authorization”, an error that could be discovered by reasoning-based formal verification. Advancing the use and applicability of automated reasoning in therefore both timely and challenging in any effort towards ensuring reliability of software technologies.

Background: ERC Consolidator Grants

The ERC Consolidator Grants are awarded to outstanding researchers of any nationality and age, with at least seven and up to twelve years of experience after PhD, and a scientific track record showing great promise. Research must be conducted in a public or private research organisation located in one of the EU Member States or “Associated” Countries. The funding – up to €2 million per grant, plus in some cases an additional €1 million for start-up costs – is provided for up to five years and mostly covers the employment of researchers and other staff to consolidate the grantees’ teams.  

About the ERC

The European Research Council, set up by the European Union in 2007, is the premiere European funding organisation for excellent frontier research. Every year, it selects and funds the very best, creative researchers of any nationality and age, to run projects based in Europe. It offers four core grant schemes: Starting, Consolidator, Advanced and Synergy Grants. With its additional Proof of Concept grant scheme, the ERC helps grantees to bridge the gap between grantees’ pioneering research and early phases of its commercialisation.

 

Comments are closed.