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:
- Clang tools for automating transformations.
- Exam corpus. Problem descriptions of exam corpus and tests.
- Competition corpus. Problem descriptions of competition corpus and tests.
- Equivalence of some classic algorithms: corpus and problem descriptions.
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