The NWO Exact and Natural Sciences board has given the green light to 18 applications in the competitive Open Competition ENW-M. The selected projects encompass critical topics such as climate model improvement, e-waste recycling, anxiety and hyperactivity in anorexia, and the study of dark matter. The aim of M-subsidies is to advance innovative, high-quality fundamental research and/or research addressing urgent scientific concerns.
One verification tool for all programming languages
Prof. Dr. Marieke Huisman, from the Formal Methods and Tool group, with the support of Dr. Ir. Vadim Zaytsev, leads the standout project Pallas: Program Analysis for LLVM-IR and All its Source languages. Pallas aims for a universal approach to ensure correctness in programming languages based on LLVM, simplifying verification tech development. This is crucial given software's pivotal role in our lives, where failures can lead to disasters and financial losses. Software developers urgently seek techniques to improve quality, especially formal verification to prevent errors. Pallas tackles integration challenges by creating deductive program verification for LLVM-IR, applicable to any programming language that compiles to this format. The project defines a generic specification format, facilitating verification and feedback at the source program level. Pallas will be rigorously evaluated through industrial case studies, highlighting its potential impact and versatility.
About the Open ENW-M Competition
The Open Competition ENW-M offers researchers the chance to explore creative and risky ideas, fostering scientific innovations that could shape future research themes. In this round (package 22-3), a total of 72 applications were considered, resulting in funding for one M-invest application, five M-2 applications, and twelve M-1 applications, recognized for their potential to significantly contribute to the scientific landscape.
