Splitting via interpolants. (English) Zbl 1326.68091
Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 186-201 (2012).
Summary: A common problem in software model checking is the automatic computation of accurate loop invariants. Loop invariants can be derived from interpolants for every path leading through the corresponding loop header. However, in practice, the consideration of single paths often leads to very path specific interpolants. Inductive invariants can only be derived after several iterations by also taking previous interpolants into account.
In this paper, we introduce a software model checking approach that uses the concept of path insensitive interpolation to compute loop invariants. In contrast to current approaches, path insensitive interpolation summarizes several paths through a program location instead of one. As a consequence, it takes the abstraction refinement considerably less effort to obtain an adequate interpolant. First experiments show the potential of our approach.
For the entire collection see [Zbl 1236.68007].
In this paper, we introduce a software model checking approach that uses the concept of path insensitive interpolation to compute loop invariants. In contrast to current approaches, path insensitive interpolation summarizes several paths through a program location instead of one. As a consequence, it takes the abstraction refinement considerably less effort to obtain an adequate interpolant. First experiments show the potential of our approach.
For the entire collection see [Zbl 1236.68007].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Amla, N., McMillan, K.L.: Combining Abstraction Refinement and SAT-Based Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 405–419. Springer, Heidelberg (2007) · Zbl 1186.68274 · doi:10.1007/978-3-540-71209-1_31 |
| [2] | Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: POPL, pp. 1–3. ACM, New York (2002) |
| [3] | Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. SIGSOFT Softw. Eng. Notes 31, 82–87 (2005) · doi:10.1145/1108768.1108813 |
| [4] | Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25–32 (2009) · doi:10.1109/FMCAD.2009.5351147 |
| [5] | Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast: Applications to software engineering. Int. J. Softw. Tools Technol. Transf. 9, 505–525 (2007) · doi:10.1007/s10009-007-0044-z |
| [6] | Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011) · doi:10.1007/978-3-642-22110-1_16 |
| [7] | Bradley, A., Manna, Z., Sipma, H.: What’s Decidable About Arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005) · Zbl 1176.68116 · doi:10.1007/11609773_28 |
| [8] | Brückner, I., Dräger, K., Finkbeiner, B., Wehrheim, H.: Slicing Abstractions. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 17–32. Springer, Heidelberg (2007) · Zbl 1141.68457 · doi:10.1007/978-3-540-75698-9_2 |
| [9] | Bruttomesso, R., Ghilardi, S., Ranise, S.: Rewriting-based quantifier-free interpolation for a theory of arrays. In: RTA, pp. 171–186 (2011) · Zbl 1236.68179 |
| [10] | Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005) · Zbl 1087.68586 · doi:10.1007/978-3-540-31980-1_40 |
| [11] | Dräger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 271–274. Springer, Heidelberg (2010) · doi:10.1007/978-3-642-12002-2_22 |
| [12] | Kroening, D., Weissenbacher, G.: Interpolation-Based Software Verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 573–578. Springer, Heidelberg (2011) · doi:10.1007/978-3-642-22110-1_45 |
| [13] | Leino, K.R.M.: This is Boogie 2. Manuscript KRML 178 (2008), http://research.microsoft.com/ leino/papers.html |
| [14] | McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) · Zbl 1278.68184 · doi:10.1007/978-3-540-45069-6_1 |
| [15] | McMillan, K.L.: Applications of Craig Interpolants in Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005) · Zbl 1087.68597 · doi:10.1007/978-3-540-31980-1_1 |
| [16] | McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006) · Zbl 1188.68196 · doi:10.1007/11817963_14 |
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.
