Automated reasoning group


Overview | More on LAV | Download | LAV in education | Contact


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).

Parallelization of Software Verification Tool LAV was presented at Types for Proofs and Programs 2017 [pdf]

Modelling used in LAV was presented at Type Theory Based Tools, 2017 [pdf]

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

Download LAV

Source code: LAV v1.4

Please read the README.txt file where you will find all neccessary instructions on how to compile and how to use LAV.

Some corpora

Corpus 1 and corpus 2 used for evaluation in the VSTTE 2012 paper.
Corpus, results and scripts used for experimenting with parallelization within LAV.

LAV in education

Exam corpus and competition corpus used for regression verification with LAV - Regression Verification for Automated Evaluation of Students’ Programs. Problem descriptions of exam corpus and tests. Clang tools. Problem descriptions of competition corpus and tests. Equivalence of some classic algorithms.

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]

Corpus and similarity tool (developed by Mladen Nikolic) described in the paper: Software Verification and Graph Similarity for Automated Evaluation of Students' Programs, Information and Software Technology, Elsevier, 2013, [ DOI ]

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
prof Filip Maric, Univ. of Belgrade
Branislava Zivkovic, Univ. of Belgarde

For more information, please contact Milena Vujosevic Janicic, mail: milena _at_