Verifying heap-manipulating programs in an SMT framework. (English) Zbl 1141.68484
Namjoshi, Kedar S. (ed.) et al., Automated technology for verification and analysis. 5th international symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75595-1/pbk). Lecture Notes in Computer Science 4762, 237-252 (2007).
Summary: Automated software verification has made great progress recently, and a key enabler of this progress has been the advances in efficient, automated decision procedures suitable for verification (Boolean satisfiability solvers and satisfiability-modulo-theories (SMT) solvers). Verifying general software, however, requires reasoning about unbounded, linked, heap-allocated data structures, which in turn motivates the need for a logical theory for such structures that includes unbounded reachability. So far, none of the available SMT solvers supports such a theory. In this paper, we present our integration of a decision procedure that supports unbounded heap reachability into an available SMT solver. Using the extended SMT solver, we can efficiently verify examples of heap-manipulating programs that we could not verify before.
For the entire collection see [Zbl 1138.68006].
For the entire collection see [Zbl 1138.68006].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Ackermann, W., Solvable Cases of the Decision Problem, Studies in Logic and the Foundations of Mathematics (1954), Amsterdam: North-Holland, Amsterdam · Zbl 0056.24505 |
| [2] | Babić, D.; Hu, A. J.; Damm, W.; Hermanns, H., Structural abstraction of software verification conditions, CAV 2007, 366-378 (2007), Heidelberg: Springer, Heidelberg · Zbl 1135.68463 |
| [3] | Balaban, I.; Pnueli, A.; Zuck, L.; Cousot, R., Shape analysis by predicate abstraction, VMCAI 2005 (2005), Heidelberg: Springer, Heidelberg · Zbl 1111.68396 |
| [4] | Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 203-213 (2001) |
| [5] | Barnett, M.; Leino, K. R.M.; Schulte, W.; Barthe, G.; Burdy, L.; Huisman, M.; Lanet, J. L.; Muntean, T., The Spec# programming system: An overview, CASSIS 2004 (2005), Heidelberg: Springer, Heidelberg |
| [6] | Benedikt, M.; Reps, T.; Sagiv, M.; Swierstra, S. D., A decidable logic for describing linked data structures, ESOP 1999 (1999), Heidelberg: Springer, Heidelberg |
| [7] | Beyer, D.; Henzinger, T. A.; Théoduloz, G.; Ball, T.; Jones, R. B., Lazy shape analysis, CAV 2006, 532-546 (2006), Heidelberg: Springer, Heidelberg |
| [8] | Beyer, D.; Henzinger, T. A.; Théoduloz, G.; Damm, W.; Hermanns, H., Configurable software verification: Concretizing the convergence of model checking and program analysis, CAV 2007, 504-518 (2007), Heidelberg: Springer, Heidelberg · Zbl 1135.68466 |
| [9] | Bingham, J.; Rakamarić, Z.; Emerson, E. A.; Namjoshi, K. S., A logic and decision procedure for predicate abstraction of heap-manipulating programs, VMCAI 2006, 207-221 (2005), Heidelberg: Springer, Heidelberg · Zbl 1176.68113 |
| [10] | Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T.; Rossum, P. V.; Ranise, S.; Sebastiani, R.; Etessami, K.; Rajamani, S. K., Efficient satisfiability modulo theories via delayed theory combination, CAV 2005, 335-349 (2005), Heidelberg: Springer, Heidelberg · Zbl 1081.68610 |
| [11] | Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T.; Rossum, P. V.; Ranise, S.; Sebastiani, R., Efficient theory combination via boolean search, Information and Computation, 204, 1493-1525 (2006) · Zbl 1137.68578 · doi:10.1016/j.ic.2005.05.011 |
| [12] | Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T.; Rossum, P. V.; Schulz, S.; Sebastiani, R.; Nieuwenhuis, R., The MathSAT 3 system, CADE 2005, 315-321 (2005), Heidelberg: Springer, Heidelberg |
| [13] | Bruttomesso, R.; Cimatti, A.; Franzén, A.; Griggio, A.; Sebastiani, R.; Hermann, M.; Voronkov, A., Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis, LPAR 2006, 527-541 (2006), Heidelberg: Springer, Heidelberg · Zbl 1165.68483 |
| [14] | Charlton, N.; Huth, M.; Damm, W.; Hermanns, H., Hector: Software model checking with cooperating analysis plugins, CAV 2007, 168-172 (2007), Heidelberg: Springer, Heidelberg |
| [15] | Chatterjee, S.; Lahiri, S. K.; Qadeer, S.; Rakamarić, Z.; Grumberg, O.; Huth, M., A reachability predicate for analyzing low-level software, TACAS 2007, 19-33 (2007), Heidelberg: Springer, Heidelberg · Zbl 1186.68108 |
| [16] | Clarke, E.; Kroening, D.; Sharygina, N.; Yorav, K., Predicate abstraction of ANSI-C programs using SAT, Formal Methods in System Design, 25, 2-3, 105-127 (2004) · Zbl 1090.68022 · doi:10.1023/B:FORM.0000040025.89719.f3 |
| [17] | Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking, Technical Report HPL-2003-148, HP Labs, Palo Alto, CA (2003) · Zbl 1323.68462 |
| [18] | Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 234-245 (2002) |
| [19] | Graf, S.; Saidi, H.; Grumberg, O., Construction of abstract state graphs with PVS, CAV 1997 (1997), Heidelberg: Springer, Heidelberg |
| [20] | Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL. Symp. on Principles of Programming Languages, pp. 58-70 (2002) · Zbl 1323.68374 |
| [21] | Immerman, N.; Rabinovich, A.; Reps, T.; Sagiv, M.; Yorsh, G.; Marcinkowski, J.; Tarlecki, A., The boundary between decidability and undecidability for transitive closure logics, CSL 2004, 160-174 (2004), Heidelberg: Springer, Heidelberg · Zbl 1095.03008 |
| [22] | Ivančić, F., Shlyakhter, I., Gupta, A., Ganai, M.K., Kahlon, V., Wang, C., Yang, Z.: Model checking C programs using F-Soft. In: ICCD. Intl. Conf. on Computer Design, pp. 297-308 (2005) |
| [23] | Jensen, J.L., Jørgensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 226-236 (1997) |
| [24] | Klarlund, N.; Møller, A.; Schwartzbach, M. I.; Yu, S.; Păun, A., MONA implementation secrets, CIAA 2000 (2001), Heidelberg: Springer, Heidelberg · Zbl 0989.03500 |
| [25] | Krstić, S.; Goel, A.; Grundy, J.; Tinelli, C.; Grumberg, O.; Huth, M., Combined satisfiability modulo parametric theories, TACAS 2007, 602-617 (2007), Heidelberg: Springer, Heidelberg · Zbl 1186.68297 |
| [26] | Lahiri, S. K.; Nieuwenhuis, R.; Oliveras, A.; Ball, T.; Jones, R. B., SMT techniques for fast predicate abstraction, CAV 2006, 413-426 (2006), Heidelberg: Springer, Heidelberg |
| [27] | Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL. Symp. on Principles of Programming Languages, pp. 115-126 (2006) · Zbl 1369.68143 |
| [28] | Lahiri, S.K., Qadeer, S.: A decision procedure for well-founded reachability, Microsoft Research Tech Report MSR-TR-2007-43 (2007) |
| [29] | Lev-Ami, T.; Immerman, N.; Reps, T. W.; Sagiv, M.; Srivastava, S.; Yorsh, G.; Nieuwenhuis, R., Simulating reachability using first-order logic with applications to verification of linked data structures, CADE 2005 (2005), Heidelberg: Springer, Heidelberg · Zbl 1135.68556 |
| [30] | Lev-Ami, T.; Sagiv, M.; Palsberg, J., TVLA: A system for implementing static analyses, SAS 2000, 280-301 (2000), Heidelberg: Springer, Heidelberg · Zbl 0966.68580 |
| [31] | Manevich, R.; Yahav, E.; Ramalingam, G.; Sagiv, M.; Cousot, R., Predicate abstraction and canonical abstraction for singly-linked lists, VMCAI 2005, 181-198 (2005), Heidelberg: Springer, Heidelberg · Zbl 1111.68398 |
| [32] | Manna, Z.; Zarba, C. G.; Aichernig, B. K.; Maibaum, T. S.E., Combining decision procedures, 10th Anniversary Colloquium of UNU/IIST, 381-422 (2003), Heidelberg: Springer, Heidelberg · Zbl 1274.68078 |
| [33] | McPeak, S.; Necula, G. C.; Etessami, K.; Rajamani, S. K., Data structure specifications via local equality axioms, CAV 2005, 476-490 (2005), Heidelberg: Springer, Heidelberg · Zbl 1081.68584 |
| [34] | Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 221-231 (2001) |
| [35] | Nelson, G.: Techniques for program verification. PhD thesis, Stanford University (1979) |
| [36] | Nelson, G.: Verifying reachability invariants of linked structures. In: POPL. Symp. on Principles of Programming Languages, pp. 38-47 (1983) |
| [37] | Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 2, 245-257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079 |
| [38] | Rakamarić, Z., Bingham, J., Hu, A.: A better logic and decision procedure for predicate abstraction of heap-manipulating programs, UBC Dept. Comp. Sci. Tech Report TR-2006-02 (2006), http://www.cs.ubc.ca/cgi-bin/tr/2006/TR-2006-02 · Zbl 1176.68113 |
| [39] | Rakamarić, Z.; Bingham, J.; Hu, A. J.; Cook, B.; Podelski, A., An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures, VMCAI 2007, 106-121 (2007), Heidelberg: Springer, Heidelberg · Zbl 1132.68354 |
| [40] | Ranise, S., Zarba, C.G.: A theory of singly-linked lists and its extensible decision procedure. In: SEFM. IEEE Intl. Conf. on Software Engineering and Formal Methods (2006) |
| [41] | Yorsh, G.; Rabinovich, A.; Sagiv, M.; Meyer, A.; Bouajjani, A.; Aceto, L.; Ingólfsdóttir, A., A logic of reachable patterns in linked data-structures, FOSSACS 2006 (2006), Heidelberg: Springer, Heidelberg · Zbl 1180.68131 |
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.
