Development and Evaluation of LAV: an SMT-Based Error Finding Platform

paper ps   
We present design and evaluation of LAV, a new open-source tool for statically checking program assertions and errors. LAV integrates into the popular LLVM infrastructure for compilation and analysis. LAV uses symbolic execution to construct a first-order logic formula that models the behavior of each basic blocks. It models the relationships between basic blocks using propositional formulas. By combining these two kinds of formulas LAV generates polynomial-sized verification conditions for loop-free code. It uses underapproximating or overapproximating unrolling to handle loops. LAV can pass generated verification conditions to one of the several SMT solvers: Boolector, MathSAT, Yices, and Z3. Our experiments with small 200 benchmarks suggest that LAV is competitive with related tools, so it can be used as an effective alternative for certain verification tasks. The experience also shows that LAV provides significant help in analyzing student programs and providing feedback to students in everyday university practice.

Citation

Milena Vujošević-Janičić and Viktor Kuncak. Development and evaluation of LAV: an SMT-based error finding platform. In Verified Software: Theories, Tools and Experiments (VSTTE), LNCS, 2012.

BibTex Entry

@inproceedings{VujosevicJanicicKuncak12DevelopmentandEvaluationofLAV,
  author = {Milena Vujo\v{s}evi\'{c}-Jani\v{c}i\'{c} and Viktor Kuncak},
  title = {Development and Evaluation of {LAV}: an {SMT}-Based Error Finding Platform},
  booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
  year = 2012,
  series = {LNCS},
  abstract = {We present design and evaluation of LAV, a new open-source tool 
for statically checking program assertions and errors. LAV integrates into 
the popular LLVM infrastructure for compilation and analysis. LAV uses symbolic execution to construct a first-order logic formula that models the behavior
of each basic blocks. It models the relationships between basic blocks using 
propositional formulas. By combining these two kinds of formulas LAV generates 
polynomial-sized verification conditions for loop-free code. It uses 
underapproximating or overapproximating unrolling to handle loops. LAV can 
pass generated verification conditions to one of the several SMT solvers: 
Boolector, MathSAT, Yices, and Z3. Our experiments with small 200 benchmarks 
suggest that LAV is competitive with related tools, so it can be used as an 
effective alternative for certain verification tasks. The experience also 
shows that LAV provides significant help in analyzing student programs and providing feedback to students in everyday university practice.}
}