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
Descripción
Sumario: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.

Ejemplares similares