UNIVERSITY OF BELGRADE
DEPARTMENT FOR COMPUTER SCIENCE

ARGO

Automated reasoning group

LAV

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

Overview

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]

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, concurrent LAV and SQLAV

Concurrent Bug Finding in LAV

Milena Vujošević Janičić: Concurrent Bug Finding Based on Bounded Model Checking. Int. J. Softw. Eng. Knowl. Eng. 30(5): 669-694 (2020). DOI:10.1142/S0218194020500242

First steps towards making concurrent solution for the tool LAV was presented at Types for Proofs and Programs 2017. [pdf]

Download concurrent version of LAV.

Corpora used for evaluation in Concurrent Bug Finding Based on Bounded Model Checking and detailed results.

SQLAV framework

Mirko Spasić, Milena Vujošević Janičić: Verification supported refactoring of embedded SQL. Software Quality Journal (2020). DOI: 10.1007/s11219-020-09517-y

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

Milena Vujošević Janičić, Filip Marić: Regression verification for automated evaluation of students programs. Comput. Sci. Inf. Syst. 17(1): 205-227 (2020). DOI: 10.2298/CSIS181220019V

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.

Source code: LAV with support for parallelization

Source code: SQLAV framework

Some corpora

Corpora used for evaluation in Concurrent Bug Finding Based on Bounded Model Checking and detailed results.
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.

Contact

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_ matf.bg.ac.rs