VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution)

Priyanka Darke, Sakshi Agrawal, R. Venkatesh

2021Lecture notes in computer science28 citationsDOI Open Access PDF

Abstract

Abstract VeriAbs is a strategy selection-based reachability verifier for C programs. The selection of a suitable strategy is from a pre-defined set of strategies and by taking into account the syntax and semantics of the code to be verified. This year we present VeriAbs version 1.4.1 in which a novel preprocessor to strategy selection is introduced. The preprocessor checks for the feasibility of performing a lightweight slicing of the input code using function call graph and variable reference information. By this if the program is found to be sliceable , sub-programs or slices are generated, and the known strategy selection algorithm of VeriAbs is applied to each slice. The verification results of each slice are then composed to derive that of the entire program. This compositional verification has improved the scalability of VeriAbs and presented in this paper.

Topics & Concepts

Computer scienceProgram slicingReachabilityScalabilityPreprocessorProgramming languageCall graphSlicingSelection (genetic algorithm)GraphSemantics (computer science)SyntaxCode (set theory)Set (abstract data type)Theoretical computer scienceArtificial intelligenceDebuggingDatabaseWorld Wide WebSoftware Testing and Debugging TechniquesFormal Methods in VerificationLogic, programming, and type systems