Abstraction refinement for quantified array assertions. (English) Zbl 1248.68151

Seghir, Mohamed Nassim; Podelski, Andreas; Wies, Thomas

Palsberg, Jens (ed.) et al., Static analysis. 16th international symposium, SAS 2009, Los Angeles, CA, USA, August 9–11, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03236-3/pbk). Lecture Notes in Computer Science 5673, 3-18 (2009).

Summary: We present an abstraction refinement technique for the verification of universally quantified array assertions such as “all elements in the array are sorted”. Our technique can be seamlessly combined with existing software model checking algorithms. We implemented our technique in the ACSAR software model checker and successfully verified quantified array assertions for both text book examples and real-life examples taken from the Linux operating system kernel.
For the entire collection see [Zbl 1169.68005].

MSC:

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

Software:

ARMC; SLAM; ACSAR

References:

[1]	Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 158–172. Springer, Heidelberg (2002) · Zbl 1043.68523
[2]	Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1–3 (2002) · Zbl 06416251
[3]	Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007) · Zbl 1132.68333
[4]	Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300–309 (2007)
[5]	Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE, pp. 385–395 (2003)
[6]	Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000) · Zbl 0974.68517
[7]	Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006) · Zbl 05187406
[8]	Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002) · Zbl 1323.68371
[9]	Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: POPL, pp. 338–350 (2005) · Zbl 1369.68138
[10]	Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
[11]	Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235–246 (2008) · Zbl 1295.68085
[12]	Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232–244 (2004) · Zbl 1325.68147
[13]	Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002) · Zbl 1323.68374
[14]	Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007) · Zbl 1135.68474
[15]	Kovacs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, G. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–486. Springer, Heidelberg (2009) · Zbl 05535552
[16]	Kuncak, V., Rinard, M.: Boolean Algebra of Shape Analysis Constraints. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 59–72. Springer, Heidelberg (2004) · Zbl 1202.68250
[17]	Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004) · Zbl 1202.68251
[18]	Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004) · Zbl 1103.68627
[19]	Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005) · Zbl 1111.68398
[20]	McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008) · Zbl 1134.68416
[21]	Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006)
[22]	Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 268–283. Springer, Heidelberg (2005) · Zbl 1141.68374
[23]	Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS (2002) · Zbl 1103.68635
[24]	Seghir, M.N., Podelski, A.: ACSAR: Software model checking with transfinite refinement. In: SPIN, pp. 274–278 (2007)
[25]	Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI (to appear, 2009)
[26]	Yorsh, G., Reps, T.W., Sagiv, M., Wilhelm, R.: Logical Characterizations of Heap Abstractions. ACM Transactions on Computational Logic 8(1) (2007) · Zbl 1367.68078