VeriAbs : Verification by Abstraction and Test Generation
Abstract
Verification of programs continues to be a challenge and no single known technique succeeds on all programs. In this paper we present VeriAbs, a reachability verifier for C programs that incorporates a portfolio of techniques implemented as four strategies, where each strategy is a set of techniques applied in a specific sequence. It selects a strategy based on the kind of loops in the program. We analysed the effectiveness of the implemented strategies on the 3831 verification tasks from the ReachSafety category of the 8th International Competition on Software Verification (SV-COMP) 2019 and found that although classic techniques - explicit state model checking and bounded model checking, succeed on a majority of the programs, a wide range of further techniques are required to analyse the rest. A screencast of the tool is available at https://youtu.be/Hzh3PPiODwk.
BibTeX
@inproceedings{Afzal-al:ASE19,
author = {Mohammad Afzal and
Asia A and
Avriti Chauhan and
Bharti Chimdyalwar and
Priyanka Darke and
Advaita Datar and
Shrawan Kumar and
R. Venkatesh},
title = {{VeriAbs} : Verification by Abstraction and Test Generation},
booktitle = {ASE},
pages = {1138--1141},
publisher = {{IEEE}},
year = {2019},
}