Automatic Verification of LLVM Code

TL;DR

This paper introduces Lodin, a comprehensive software verification tool for LLVM code that integrates explicit, statistical, and symbolic model checking techniques to improve verification effectiveness.

Contribution

The paper presents Lodin, a novel verification tool combining multiple model checking algorithms specifically for LLVM code analysis.

Findings

Lodin successfully verifies LLVM programs using combined techniques.

The tool demonstrates improved accuracy over single-method approaches.

Lodin supports various verification scenarios with promising results.

Abstract

In this work we present our work in developing a software verification tool for llvm-code - Lodin - that incorporates both explicit-state model checking, statistical model checking and symbolic state model checking algorithms.