×

Data abstraction: a general framework to handle program verification of data structures. (English) Zbl 1497.68108

Drăgoi, Cezara (ed.) et al., Static analysis. 28th international symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12913, 215-235 (2021).
Summary: Proving properties on programs accessing data structures such as arrays often requires universally quantified invariants, e.g., “all elements below index \(i\) are nonzero”. In this article, we propose a general data abstraction scheme operating on Horn formulas, into which we recast previously published abstractions. We show that our instantiation scheme is relatively complete: the generated purely scalar Horn clauses have a solution (inductive invariants) if and only if the original problem has one expressible by the abstraction.
For the entire collection see [Zbl 1489.68011].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

FunArray; SeaHorn; z3; JayHorn
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Beyer, D.; Beyer, D.; Huisman, M.; Kordon, F.; Steffen, B., Automatic verification of C and Java programs: SV-COMP 2019, Tools and Algorithms for the Construction and Analysis of Systems, 133-155 (2019), Cham: Springer, Cham · doi:10.1007/978-3-030-17502-3_9
[2] Bjørner, N.; McMillan, K.; Rybalchenko, A.; Logozzo, F.; Fähndrich, M., On solving universally quantified horn clauses, Static Analysis, 105-125 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-38856-9_8
[3] Bradley, AR; Manna, Z.; Sipma, HB; Emerson, EA; Namjoshi, KS, What’s decidable about arrays?, Verification, Model Checking, and Abstract Interpretation, 427-442 (2005), Heidelberg: Springer, Heidelberg · Zbl 1176.68116 · doi:10.1007/11609773_28
[4] Braine, J., Gonnord, L., Monniaux, D.: Data Abstraction: A General Framework to Handle Program Verification of Data Structures. Research Report RR-9408, Inria Grenoble Rhône-Alpes; VERIMAG UMR 5104, Université Grenoble Alpes, France; LIP - Laboratoire de l’Informatique du Parallélisme; Université Lyon 1 - Claude Bernard; ENS Lyon, May 2021. https://hal.inria.fr/hal-03214475
[5] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977) · Zbl 1149.68389
[6] Cousot, P.; Cousot, R.; Logozzo, F., A parametric segmentation functor for fully automatic and scalable array content analysis, SIGPLAN Not., 46, 1, 105-118 (2011) · Zbl 1284.68210 · doi:10.1145/1925844.1926399
[7] Dillig, I.; Dillig, T.; Aiken, A.; Gordon, AD, Fluid updates: beyond strong vs. weak updates, Programming Languages and Systems, 246-266 (2010), Heidelberg: Springer, Heidelberg · Zbl 1250.90057 · doi:10.1007/978-3-642-11957-6_14
[8] Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: PLDI (2005) · Zbl 1369.68138
[9] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.: The SeaHorn verification framework. In: CAV (2015)
[10] Gurfinkel, A.; Shoham, S.; Vizel, Y.; Lahiri, SK; Wang, C., Quantifiers on demand, Automated Technology for Verification and Analysis, 248-266 (2018), Cham: Springer, Cham · Zbl 1517.68239 · doi:10.1007/978-3-030-01090-4_15
[11] Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008). Association for Computing Machinery, New York, NY, USA (2008)
[12] Hojjat, H., Rümmer, P.: The ELDARICA horn solver. In: FMCAD (2018)
[13] Ish-Shalom, O.; Itzhaky, S.; Rinetzky, N.; Shoham, S.; Beyer, D.; Zufferey, D., Putting the squeeze on array programs: loop verification via inductive rank reduction, Verification, Model Checking, and Abstract Interpretation, 112-135 (2020), Cham: Springer, Cham · Zbl 07228504 · doi:10.1007/978-3-030-39322-9_6
[14] Kahsai, T., Rümmer, P., Schäf, M.: JayHorn: A Java Model Checker: (Competition Contribution) (2019)
[15] Kroening, D.; Strichman, O., Decision Procedures (2008), Heidelberg: Springer, Heidelberg · Zbl 1149.68071 · doi:10.1007/978-3-540-74105-3
[16] Monniaux, D.; Alberti, F.; Blazy, S.; Jensen, T., A simple abstraction of arrays and maps by program translation, Static Analysis, 217-234 (2015), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-662-48288-9_13
[17] Monniaux, D.; Gonnord, L.; Rival, X., Cell morphing: from array programs to array-free horn clauses, Static Analysis, 361-382 (2016), Heidelberg: Springer, Heidelberg · Zbl 1394.68081 · doi:10.1007/978-3-662-53413-7_18
[18] de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.