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

Mohammad Atif Faiz Afzal, Supratik Chakraborty, Avriti Chauhan, Bharti Chimdyalwar, Priyanka Darke, Ashutosh Gupta, Shrawan Kumar, Charles Babu M, Divyesh Unadkat, R. Venkatesh

2020Lecture notes in computer science16 citationsDOI Open Access PDF

Abstract

Abstract 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.

Topics & Concepts

Computer scienceReachabilityPruningAbstractionAutomatic summarizationLoop (graph theory)Path (computing)Code (set theory)Formal verificationProgramming languageSelection (genetic algorithm)Theoretical computer scienceAlgorithmArtificial intelligenceSet (abstract data type)BiologyPhilosophyCombinatoricsAgronomyMathematicsEpistemologyFormal Methods in VerificationSoftware Testing and Debugging TechniquesLogic, programming, and type systems