Limited-Time Offer: Up to 75% Off Coursera Plus!
7000+ certificate courses from Google, Microsoft, IBM, and many more.
This course aims to teach learners how to verify LLVM-based tools such as compilers, optimizers, and code instrumentation passes, especially for safety or security critical applications. The course covers understanding LLVM intermediate representation from a programming language semantics perspective and using Vellvm to develop machine-checkable formal properties about LLVM IR programs and transformation passes. The teaching method involves exploring LLVM code, including its complex aspects, and demonstrating how interactive theorem provers like Coq can be used for verification. The intended audience for this course includes individuals interested in LLVM, formal verification technologies, and compiler transformations, with no prior experience assumed.
