Presentation: Logic-Based Automated Reasoning

Developing efficient and scalable software analysis tools is a tedious and very difficult task. First, due to the undecidability of the verification problem, tools, must be highly tuned and engineered to provide reasonable efficiency and precision trade-offs. Second, different programming languages come with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult. In this talk, I will present SeaHorn — an open source automated logic-based reasoning tool built on top of LLVM -- an industrial compiler infrastructure. SeaHorn combines traditional and advanced automated reasoning algorithms based on Satisfiability Modulo Theory (SMT) and Abstract Interpretation. SeaHorn is a versatile and highly customizable tool which allows developers to easily build or experiment with new verification techniques.