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.
P. Darke—Jury member
Chapter PDF
Similar content being viewed by others
References
TCS Research. http://www.tcs.com/research/Pages/default.aspx
Afzal, M., Asia, A., Chauhan, A., Chimdyalwar, B., Darke, P., Datar, A., Kumar, S., Venkatesh, R.: VeriAbs: Verification by Abstraction and Test Generation. In: ASE. pp. 1138–1141 (2019)
Audemard, G., Simon, L.: On the glucose sat solver. IJAIT 27(01) (2018)
Bardin, A., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: ATVA. pp. 474–488 (2005)
Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction withcontinuously-refined invariants. In: CAV. pp. 622–640 (2015)
Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programsby tiling. In: SAS. pp. 428–449 (2017)
Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programswith full-program induction. In: TACAS (2020)
Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In:TACAS (2004)
Darke, P., Prabhu, S., Chimdyalwar, B., Chauhan, A., Kumar, S., Basakchowdhury,A., Venkatesh, R., Datar, A., Medicherla, R.K.: VeriAbs: Verification byAbstraction and Test Generation - (Competition Contribution). In: TACAS. pp.457–462 (2018)
De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: TACAS. pp.337–340 (2008)
Heizmann, M., Chen, Y., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y.,Nutz, A., Musa, B., Schilling, C., Schindler, T., Podelski, A.: Ultimateautomizer and the search for perfect interpolants - (competitioncontribution). In: TACAS. pp. 447–451 (2018)
Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration ofgeneral linear loops. SIGPLAN Not. 49(1), 529–540 (2014)
Khare, S., Saraswat, S., Kumar, S.: Static program analysis of large embeddedcode base: an experience. In: ISEC. pp. 99–102 (2011)
Kumar, S.: Scaling up Property Checking.https://www.cse.iitb.ac.in/~as/thesis_soft.pdf (2019)
Lattner, C.: LLVM and Clang: Next generation compiler technology. In: The BSDConference (2008)
Zalewski, M.: 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
© 2020 The Author(s)
About this paper
Cite this paper
Afzal, M. et al. (2020). VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution). In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)