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.

Thesis_Mtech_CS_4028.pdf - Published Version

Download (4MB) | Preview


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:
IITH CreatorsORCiD
Item Type: Thesis (Masters)
Uncontrolled Keywords: LLVM, Cprover, Model Check
Subjects: Computer science
Divisions: Department of Computer Science & Engineering
Depositing User: Team Library
Date Deposited: 18 Jun 2018 04:51
Last Modified: 18 Jun 2018 04:51
URI: http://raiith.iith.ac.in/id/eprint/4028
Publisher URL:
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 4028 Statistics for this ePrint Item