Automated reasoning group


Overview | More on LAV | SQLAV | 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).

A calculus for a LLVM-based software verification tool LAV was presented at EUTypes meeting, Nijmegen, Netherlands, 22-24 January 2018. [pdf]

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

See also section LAV in education

SQLAV framework

First steps towards proving functional equivalence of embedded SQL. Presented at 24th International Conference on Types for Proofs and Programs,TYPES 2018. [pdf]

Download SQLAV framework
Corpus used for evaluation in Verification Supported Refactoring of Embedded SQL and detailed results.

LAV in education

Regression Verification for Automated Evaluation of Students’ Programs:

  1. Clang tools for automating transformations.
  2. Exam corpus. Problem descriptions of exam corpus and tests.
  3. Competition corpus. Problem descriptions of competition corpus and tests.
  4. Equivalence of some classic algorithms: corpus and problem descriptions.

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

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 used for evaluation in Verification Supported Refactoring of Embedded SQL and detailed results.
Examples (used in "First steps towards proving functional equivalence of embedded SQL") and formulas jointly generated by SQL2SMT tool and LAV for automated checking of functional equivalence of embedded SQL functions (used in "First steps towards proving functional equivalence of embedded SQL").
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 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_