University of Twente Student Theses


VCLLVM: A Transformation Tool for LLVM IR programs to aid Deductive Verification

Oorschot, D.H.M.A. van (2023) VCLLVM: A Transformation Tool for LLVM IR programs to aid Deductive Verification.

[img] PDF
Abstract:Errors in computer programs are as old as the discipline of computer programming itself. While the nature of these errors has changed over time, the fact remains that computer bugs will never be eliminated. For this reason, research into software verification techniques is essential for the future of software development. Verification techniques come in many forms. VerCors is a verification toolset that uses deductive verification for languages such as Java, C, and its own internal PVL (Prototypal Verification Language). However, developing and maintaining support for a language adds significant development overhead to the project, as semantic models must be defined and updated separately for each language. This thesis presents VCLLVM, a project that adds LLVM IR as a supported language to the VerCors toolset. Having LLVM IR supported as a language opens future possibilities for verifying any language that is compiled through the LLVM infrastructure. Moreover, the tandem of VCLLVM/VerCors would bring novel research to the field of software verification as to the best of our knowledge, it is the first deductive verifier for LLVM IR.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page