Clone wiki

llStar / Home

About llStar

NEW: Try llStar online with the llStar Web app!

llStar is an automatic prover for programs written in LLVM IR. LLVM IR is the intermediate representation of the LLVM compiler framework. llStar attempts to prove individual functions correct with respect to memory safety and to their specifications. In doing so, it automatically discovers loop invariants. Specifications are pre and post-conditions for each function, written in the formalism of separation logic. They are given by the user, or can in some cases be inferred by llStar.

Getting started

The easiest way to start using llStar is via its Web interface.

To install llStar on your own machine, see the installation document.

For more information, see the Usage and Architecture documents.

Come get help on IRC: #llstar on


llStar is distributed under a 3-clause BSD licence (see LICENSE ).