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.
The easiest way to start using llStar is via its Web interface.
To install llStar on your own machine, see the installation document.
Come get help on IRC: #llstar on irc.oftc.net.
llStar is distributed under a 3-clause BSD licence (see LICENSE ).