OC-M grant for Pallas: Program Analysis for LLVM-IR and All its Source languages

15-Dec-2023

Marieke Huisman, from the Formal Methods and Tool group at the University of Twente received a grant for the OC-M 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.

Marieke will work on this project with 2 PhD students (one funded by the OC-M project, one funded by internal funds). Vadim Zaytsev, also from the University of Twente, will act as a co-supervisor for the project, bringing in his expertise on compiler technology.