In this presentation we will discuss and demonstrate an approach to build various Formal Methods (FM) tools leveraging LLVM. FM has seen a significant increase in usage in software over the past decade, being used in critical system design, security, and prototyping. We will discuss the benefits and drawbacks of LLVM IR for FM and the need for an Abstract Representation (AR) that allows for the analysis via engineering approximations. In particular we want to talk about our approach and tools that mapped our chosen AR, developed at NASA, and then extending our initial set of analysis into more logical and hierarchal relationship. Lastly we want to present what we feel are the difficulties, future challenges and successes of FM tools integrating with LLVM community.
