VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)

VeriAbs is a strategy selection based reachability verifier for C code. It analyzes the structure of loops, and intervals of inputs to choose one of the four verification strategies implemented in VeriAbs. In this paper, we present VeriAbs version 1.4 with updates in three strategies. We add an arra...

Descripción completa

Detalles Bibliográficos
Autores principales: Afzal, Mohammad, Chakraborty, Supratik, Chauhan, Avriti, Chimdyalwar, Bharti, Darke, Priyanka, Gupta, Ashutosh, Kumar, Shrawan, Babu M, Charles, Unadkat, Divyesh, Venkatesh, R
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480689/
http://dx.doi.org/10.1007/978-3-030-45237-7_25
_version_ 1783580459838472192
author Afzal, Mohammad
Chakraborty, Supratik
Chauhan, Avriti
Chimdyalwar, Bharti
Darke, Priyanka
Gupta, Ashutosh
Kumar, Shrawan
Babu M, Charles
Unadkat, Divyesh
Venkatesh, R
author_facet Afzal, Mohammad
Chakraborty, Supratik
Chauhan, Avriti
Chimdyalwar, Bharti
Darke, Priyanka
Gupta, Ashutosh
Kumar, Shrawan
Babu M, Charles
Unadkat, Divyesh
Venkatesh, R
author_sort Afzal, Mohammad
collection PubMed
description VeriAbs is a strategy selection based reachability verifier for C code. It analyzes the structure of loops, and intervals of inputs to choose one of the four verification strategies implemented in VeriAbs. In this paper, we present VeriAbs version 1.4 with updates in three strategies. We add an array verification technique called full-program induction, and enhance the existing techniques of loop pruning, k-path interval analysis, and disjunctive loop summarization. These changes have improved the verification of programs with arrays, and unstructured loops and unstructured control flows.
format Online
Article
Text
id pubmed-7480689
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74806892020-09-10 VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution) Afzal, Mohammad Chakraborty, Supratik Chauhan, Avriti Chimdyalwar, Bharti Darke, Priyanka Gupta, Ashutosh Kumar, Shrawan Babu M, Charles Unadkat, Divyesh Venkatesh, R Tools and Algorithms for the Construction and Analysis of Systems Article VeriAbs is a strategy selection based reachability verifier for C code. It analyzes the structure of loops, and intervals of inputs to choose one of the four verification strategies implemented in VeriAbs. In this paper, we present VeriAbs version 1.4 with updates in three strategies. We add an array verification technique called full-program induction, and enhance the existing techniques of loop pruning, k-path interval analysis, and disjunctive loop summarization. These changes have improved the verification of programs with arrays, and unstructured loops and unstructured control flows. 2020-03-13 /pmc/articles/PMC7480689/ http://dx.doi.org/10.1007/978-3-030-45237-7_25 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Afzal, Mohammad
Chakraborty, Supratik
Chauhan, Avriti
Chimdyalwar, Bharti
Darke, Priyanka
Gupta, Ashutosh
Kumar, Shrawan
Babu M, Charles
Unadkat, Divyesh
Venkatesh, R
VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)
title VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)
title_full VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)
title_fullStr VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)
title_full_unstemmed VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)
title_short VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution)
title_sort veriabs : verification by abstraction and test generation (competition contribution)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480689/
http://dx.doi.org/10.1007/978-3-030-45237-7_25
work_keys_str_mv AT afzalmohammad veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT chakrabortysupratik veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT chauhanavriti veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT chimdyalwarbharti veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT darkepriyanka veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT guptaashutosh veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT kumarshrawan veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT babumcharles veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT unadkatdivyesh veriabsverificationbyabstractionandtestgenerationcompetitioncontribution
AT venkateshr veriabsverificationbyabstractionandtestgenerationcompetitioncontribution

Ejemplares similares