LAV (LLVM Automated Verifier) is a bug finding 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 control-flow 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.
More on LAV
For more information on what LAV is and what it can do, see the Development and Evaluation of LAV: an SMT-Based Error Finding Platform paper presented at VSTTE 2012 (slides).
LAV was presented at Fourth Workshop on Formal and Automated Theorem Proving and Applications, February 4-5, 2011 --- A New Verification Tool: From LLVM Code to SMT Formulae
Source code: LAV v1.3
Please read the README.txt file where you will find all neccessary instructions on how to compile and how to use LAV.
LAV in education
Corpus used for regression verification with LAV - Regression Verification for Automated Evaluation of Students’ Programs. Problem descriptions. Clang tools.
LAV was presented at Dagstuhl Seminar 14352, Next Generation Static Software Analysis Tools, August 24-29, Schloss Dagstuhl, Germany. System LAV and Automated Evaluation of Students’ Programs, Dagstuhl Reports, Volume 4, Issue 8, 2014. [pdf]
Similarity tool (developed by Mladen Nikolic) and corpus described in the paper: Software Verification and Graph Similarity for Automated Evaluation of Students' Programs, Information and Software Technology, Elsevier, 2013, [ DOI ]
Corpus described in the VSTTE 2012 paper.
LAVedu was presented at Fifth Workshop on Formal and Automated Theorem Proving and Applications February 3-4, 2012 --- Automated Evaluation of Students' Programs: Testing, Verification and Similarity
LAV is developed by
Milena Vujosevic-Janicic, in colaboration with
prof Dusan Tosic, Univ. of Belgrade,
prof Viktor Kuncak, EPFL Lausanne, and
prof Filip Maric, Univ. of Belgrade.
For more information, please contact Milena Vujosevic-Janicic, mail: milena _at_ matf.bg.ac.rs