Software Verification (LAV)
LAV is a software verification tool built on top of the LLVM compiler infrastructure, and available under the UIUC open source license.
LAV combines symbolic execution, SAT encoding of program's behavior and some features of bounded model checking. Namely, single blocks of the code are modelled by first-order logic formulae constructed by symbolic execution, while relationships between blocks are modelled by propositional formulae. Formulae that describe blocks' behavior are combined with correctness conditions for individual commands to produce correctness conditions of the program to be verified. These conditions are passed to a SMT solver covering a suitable combination of theories. There is support for export to linear arithmetic, bit-vector arithmetic, the theory of uninterpreted functions (and Ackermannization, as its alternative), and the theory of arrays. LAV can use the following SMT solvers: Boolector, MathSAT, Yices, and Z3. Our experiments suggest that the presented approach is competitive with related tools, so it can be used as a useful alternative for some sorts of verification tasks.
For more information on what LAV is and what it can do, see the LAV page: http://argo.matf.bg.ac.rs/?content=lav