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.
P. Darke—Jury member
Chapter PDF
Similar content being viewed by others
References
Foundations of Computing Group at TCS Research. https://www.tcs.com/designing-complex-intelligent-systems.
M. Afzal, A. Asia, A. Chauhan, B. Chimdyalwar, P. Darke, A. Datar, S. Kumar, and R Venkatesh. VeriAbs: Verification by Abstraction and Test Generation. In ASE, pages 1138–1141, 2019.
M. Afzal, S. Chakraborty, A. Chauhan, B. Chimdyalwar, P. Darke, A. Gupta,S. Kumar, C. Babu M, D. Unadkat, and R. Venkatesh. Veriabs : Verification by abstraction and test generation (competition contribution). In TACAS (2), pages 383–387, 2020.
G. Audemard and L. Simon. On the glucose sat solver. IJAIT, 27(01), 2018.
D. Beyer. Software verification: 10th comparative evaluation (SV-COMP 2021). In Proc. TACAS (2), LNCS 12652. Springer, 2021.
D. Beyer, M. Dangl, and P. Wendler. Boosting k-induction with continuously-refined invariants. In CAV, pages 622–640, 2015.
S. Chakraborty, A. Gupta, and D. Unadkat. Verifying array manipulating programs with full-program induction. In Proc. TACAS (1), pages 22–39, 2020.
B. Chimdyalwar, P. Darke, A. Chavda, S. Vaghani, and A. Chauhan. Eliminating static analysis false positives using loop abstraction and bounded model checking. In FM, pages 573–576, 2015.
E. Clarke, D. Kroening, and F. Lerda. A Tool for Checking ANSI-C Programs. In TACAS, pages 168–176, 2004.
Mark Harman and Robert M. Hierons. An overview of program slicing. Software Focus, 2(3):85–92, 2001.
M. Heizmann, Y. Chen, D. Dietsch, M. Greitschus, J. Hoenicke, Y. Li, A. Nutz,B. Musa, C. Schilling, T. Schindler, and A. Podelski. Ultimate automizer and the search for perfect interpolants - (competition contribution). In TACAS (2), pages 447–451, 2018.
S. Khare, S. Saraswat, and S. Kumar. Static program analysis of large embedded code base: an experience. In ISEC, pages 99–102, 2011.
M. Zalewski. American fuzzy lop. http://lcamtuf.coredump.cx/afl/.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
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.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Darke, P., Agrawal, S., Venkatesh, R. (2021). VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution). In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_32
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)