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.
|
PDF
3MB |
| 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: | https://purl.utwente.nl/essays/96536 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page