Funded by: NWO
Duration: 15 January 2024 until 15 January 2028
summary of the project
With the omnipresence of software, our lives and income depend crucially on the quality of software: software failures can cause planes to crash, emergency service to be unreachable, and companies to lose millions of dollars (because of missed business opportunities, but also due to reputation damage).
Therefore, software developers are urgently looking for techniques that can help them to improve the quality of their software. Formal verification techniques that allow one to prove that software will never reach an erroneous state can play an essential role in this. However, to use this in an industrial setting, we need to make sure that the verification technology can be used in combination with the newest programming language technology. Deductive program verification is a formal verification technique that works directly at the code level, and non-trivial case studies have shown its potential. However, for its widespread use, we need tool support for many different programming languages, which requires a large amount of engineering.
Therefore, Pallas advocates a different approach. Rather than building a deductive program verifier for each programming language, Pallas will develop deductive program verification technology for the widely-used intermediate representation language LLVM-IR, such that we can use deductive verification for any programming language that compiles into the LLVM-IR format. For this, we define a generic specification format to write the program specifications. The specified source program is then automatically compiled into a specified LLVM-IR program, and we verify this specified LLVM-IR program. Finally, we also develop techniques to give feedback on failed verification attempts at the level of the source program, rather than forcing the developer to study the generated LLVM-IR code. Throughout the project, the Pallas verification technology will be evaluated on various industrial case studies, including applications that use multiple programming languages, that are all targeting the LLVM-IR format.