LLVM2GOTO: A translator from LLVM IR to CPROVER IR

Sapate, Rasika Avinash and Joshi, Saurabh (2018) LLVM2GOTO: A translator from LLVM IR to CPROVER IR. Masters thesis, Indian Institute of Technology, Hyderabad.

Preview

Text
Thesis_Mtech_CS_4028.pdf - Published Version
Download (4MB) | Preview

Abstract

There are more than 700 programming languages. The number of softwares is astronomical. It is highly important to verify whether the software meets it's specification and it is safe. However, there are very few stable software verification tools. Translating a source program into verification intermediate representation(VIR) is an overhead for software verification community. If we trans- late compiler intermediate representation into VIR, the overhead of translating source to VIR is reduced and software written in programming languages supported by the compiler can be verified. LLVM2GOTO uses LLVM IR as compiler IR and CPROVER's goto IR as VIR. In the current implementation we support variable declaration, load, store, arithmetic, bitwise, typecast, branch and switch instructions are supported by LLVM2GOTO. v

[error in script]

IITH Creators: