Decision procedures for flat array properties. (English) Zbl 1356.03049
Summary: We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are parametric in the theories of indexes and elements and orthogonal with respect to known results. We show that transitive closures (‘acceleration’) of relation expressing certain array updates produce formulas inside our fragment; this observation will be used to identify a class of programs handling arrays having decidable reachability problem.
MSC:
| 03B25 | Decidability of theories and sets of sentences |
| 03B35 | Mechanization of proofs and logical operations |
| 68P05 | Data structures |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: LPAR, pp. 46-61 (2012) · Zbl 1352.68141 |
| [2] | Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-Based Abstraction for Arrays with Interpolants. In: CAV, pp. 679-685 (2012) · Zbl 1352.68141 |
| [3] | Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods in System Design 45(1), 63-109 (2014) · Zbl 1317.68107 · doi:10.1007/s10703-014-0209-9 |
| [4] | Alberti, F., Ghilardi, S., Sharygina, N.: Definability of accelerated relations in a theory of arrays and its applications. In: FroCoS, pp. 23-39 (2013) · Zbl 1397.68121 |
| [5] | Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science, pp. 18-23, Springer (2014) · Zbl 1448.68284 |
| [6] | Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: TACAS (2014) · Zbl 1356.03049 |
| [7] | Bach, E., Shallit, J.: Algorithmic Number Theory. Vol. 1. Foundations of Computing Series. MIT Press (1996) · Zbl 0873.11070 |
| [8] | Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171-177 (2011) · Zbl 1189.03046 |
| [9] | Barrett, C., Stump A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2010) |
| [10] | Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL implementation secrets. In: FTRTFT, pp. 3-22 (2002) |
| [11] | Beyer, D.; Ábrahám, E. (ed.); Havelund, K. (ed.), Status report on software verification - (competition summary sv-comp 2014), 373-388 (2014), Berlin |
| [12] | Bjørner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified horn clauses. In: SAS, pp. 105-125 (2013) · Zbl 0381.03021 |
| [13] | Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer-Verlag, Berlin (1997) · Zbl 0865.03004 · doi:10.1007/978-3-642-59207-2 |
| [14] | Bouton, T.; Caminha, D.; de Oliveira, B.; Déharbe, D.; Fontaine, P.; Schmidt, RA (ed.), Verit: An open, trustable and efficient smt-solver (2009), Berlin |
| [15] | Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae 91, 275-303 (2009) · Zbl 1189.03046 |
| [16] | Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: VMCAI, pp. 427-442 (2006) · Zbl 1176.68116 |
| [17] | Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: CAV, vol. 1427 of LNCS, pp. 268-279. Springer (1998) |
| [18] | de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS, pp. 337-340 (2008) |
| [19] | Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003) · Zbl 1323.68462 |
| [20] | Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. weak updates. In: ESOP, pp. 246-266 (2010) · Zbl 1260.68092 |
| [21] | Weber, T., Cok, D.R., Stump, A.: The 2013 SMT Evaluation. Available at http://smtcomp.sourceforge.net/2013/report/SMTEVAL-2013.pdf (2013) · Zbl 1356.68185 |
| [22] | Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: FSTTCS, pp. 145-156 (2002) · Zbl 1027.68616 |
| [23] | Ganzinger, H.: Shostak light. Automated deduction—CADE-18, vol. 2392 of Lecture Notes in Comput. Sci., pp. 332-346. Springer, Berlin (2002) · Zbl 1072.68572 |
| [24] | Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: CAV, pp. 306-320 (2009) · Zbl 1242.68280 |
| [25] | Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science 6(4) (2010) · Zbl 1213.68379 |
| [26] | Ghilardi, S., Ranise, S.: MCMT: A Model Checker Modulo Theories. In: IJCAR, pp. 22-29 (2010) · Zbl 1291.68257 |
| [27] | Habermehl, P., Iosif, R., Vojnar, T.: A logic of singly indexed arrays. In: LPAR, pp. 558-573 (2008) · Zbl 1182.03032 |
| [28] | Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: FOSSACS (2008) · Zbl 1139.03007 |
| [29] | Halpern, J.Y.: Presburger arithmetic with unary predicates is \({\varPi^1_1}\) complete. J. Symbolic Logic 56(2), 637-642 (1991) · Zbl 0738.03017 · doi:10.2307/2274706 |
| [30] | Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: TACAS, pp. 265-281. Springer (2008) · Zbl 1134.68410 |
| [31] | Jhala, R., McMillan, K.L.: Array Abstractions from Proofs. In: CAV (2007) · Zbl 1135.68474 |
| [32] | Lewis, H.B.: Complexity of solvable cases of the decision problem for the predicate calculus. In: 19th Ann. Symp. on Found. of Comp. Sci., pp. 35-47. IEEE (1978) |
| [33] | McCarthy, J.: Towards a mathematical science of computation. In: International Federation for Information Processing Congress, pp. 21-28 (1962) |
| [34] | McMillan, K.L.: Lazy Abstraction with Interpolants. In: CAV (2006) · Zbl 1188.68196 |
| [35] | Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. In: CAV’05, pp. 321-334 (2005) · Zbl 1081.68629 |
| [36] | Oppen, D.C.: A superexponential upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci. 16(3), 323-332 (1978) · Zbl 0381.03021 · doi:10.1016/0022-0000(78)90021-1 |
| [37] | Reynolds, A., Tinelli, C., Goel, A., Krstic, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: CADE, pp. 377-391 (2013) · Zbl 1381.68275 |
| [38] | Rosser, B.: The n-th prime is greater than n log n. Proc. Lond. Math. Soc., II. Ser. 45, 21-44 (1938) · JFM 64.0100.04 |
| [39] | Semënov, A.L.: Logical theories of one-place functions on the set of natural numbers. Izvestiya: Mathematics 22, 587-618 (1984) · Zbl 0541.03005 · doi:10.1070/IM1984v022n03ABEH001456 |
| [40] | Shoenfield, J.R.: Mathematical logic. Association for Symbolic Logic, Urbana, IL. Reprint of the 1973 second printing (2001) · Zbl 0965.03001 |
| [41] | Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Automat. Reason. 34(3), 209-238 (2005) · Zbl 1108.03014 · doi:10.1007/s10817-005-5204-9 |
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.
