×

zbMATH — the first resource for mathematics

Verify heaps via unified model checking. (English) Zbl 1464.68209
Summary: This paper addresses the problem of verifying heap evolution properties of pointer programs. To this end, a new unified model checking approach with MSVL (Modeling, Simulation and Verification Language) and \(\mathrm{PPTL}^\mathrm{SL}\) is presented. The former is an executable subset of PTL (Projection Temporal Logic) while the latter is an extension of PPTL (Propositional Projection Temporal Logic) with separation logic. MSVL is used to model pointer programs, and \(\mathrm{PPTL}^\mathrm{SL}\) to specify heap evolution properties. Technically, on one hand, models of MSVL programs are characterized by Normal Form Graphs (NFGs). On the other hand, \(\mathrm{PPTL}^\mathrm{SL}\) is equisatisfiably reduced to its subset which can reuse the decision procedure of PPTL. Our technique is able to deal with a variety of pointer structures such as linked lists and composite structures. In addition, we implement a prototype tool by using an SMT solver as the verification engine in order to demonstrate our approach.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68P05 Data structures
Software:
TVLA; SLAM; LLBMC; SPIN; BLAST
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Burstall, R. M., Some techniques for proving correctness of programs which alter data structures, Mach. Intell., 7, 1, 23-50 (1972) · Zbl 0259.68009
[2] Cook, S. A.; Oppen, D. C., An assertion language for data structures, (Proceedings of the 2nd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (1975), ACM), 160-166
[3] Chase, D. R.; Wegman, M. N.; Zadeck, F. K., Analysis of pointers and structures, (Proceedings of the ACM SIGPLAN’90 Conference on Programming Language Design and Implementation (PLDI). Proceedings of the ACM SIGPLAN’90 Conference on Programming Language Design and Implementation (PLDI), White Plains, New York, USA, June 20-22, 1990 (1990)), 296-310
[4] Deutsch, A., Interprocedural may-alias analysis for pointers: beyond k-limiting, (Proceedings of the ACM SIGPLAN’94 Conference on Programming Language Design and Implementation (PLDI). Proceedings of the ACM SIGPLAN’94 Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida, USA, June 20-24, 1994 (1994)), 230-241
[5] Landi, W., Undecidability of static analysis, ACM Lett. Program. Lang. Syst., 1, 4, 323-337 (1992)
[6] Sagiv, S.; Reps, T. W.; Wilhelm, R., Parametric shape analysis via 3-valued logic, ACM Trans. Program. Lang. Syst., 24, 3, 217-298 (2002)
[7] Reynolds, J. C., Separation logic: a logic for shared mutable data structures, (17th Annual IEEE Symposium on Logic in Computer Science, 2002 (2002), IEEE Computer Society: IEEE Computer Society Washington, DC, USA), 55-74
[8] Ishtiaq, S. S.; O’Hearn, P. W., BI as an assertion language for mutable data structures, (Hankin, C.; Schmidt, D., POPL’01 (2001), ACM Press: ACM Press London, UK), 14-26 · Zbl 1323.68077
[9] Berdine, J.; Calcagno, C.; O’Hearn, P. W., Symbolic execution with separation logic, (Yi, K., APLAS. APLAS, Lecture Notes in Computer Science, vol. 3780 (2005), Springer: Springer Berlin, Heidelberg, Tsukuba, Japan), 52-68 · Zbl 1159.68363
[10] Distefano, D.; O’Hearn, P. W.; Yang, H., A local shape analysis based on separation logic, (Hermanns, H.; Palsberg, J., TACAS. TACAS, Lecture Notes in Computer Science, vol. 3920 (2006), Springer: Springer Berlin, Heidelberg, Vienna, Austria), 287-302 · Zbl 1180.68112
[11] Calcagno, C.; Distefano, D.; O’Hearn, P. W.; Yang, H., Compositional shape analysis by means of bi-abduction, J. ACM, 58, 6, 26 (2011) · Zbl 1281.68155
[12] Calcagno, C.; Gardner, P.; Hague, M., From separation logic to first-order logic, (Sassone, V., FOSSACS. FOSSACS, Lecture Notes in Computer Science, vol. 3441 (2005), Springer: Springer Berlin, Heidelberg, Edinburgh, UK), 395-409 · Zbl 1119.03022
[13] Manevich, R.; Yahav, E.; Ramalingam, G.; Sagiv, S., Predicate abstraction and canonical abstraction for singly-linked lists, (Verification, Model Checking, and Abstract Interpretation, 6th International Conference, Proceedings. Verification, Model Checking, and Abstract Interpretation, 6th International Conference, Proceedings, VMCAI 2005, Paris, France, January 17-19, 2005 (2005)), 181-198 · Zbl 1111.68398
[14] Lev-Ami, T.; Immerman, N.; Reps, T.; Sagiv, M.; Srivastava, S.; Yorsh, G., Simulating reachability using first-order logic with applications to verification of linked data structures, Log. Methods Comput. Sci., 5, 2, 1-30 (2009) · Zbl 1163.68010
[15] Baier, C.; Katoen, J., Principles of Model Checking (2008), MIT Press
[16] Bouajjani, A.; Habermehl, P.; Rogalewicz, A.; Vojnar, T., Abstract regular tree model checking of complex dynamic data structures, (Static Analysis, 13th International Symposium, Proceedings. Static Analysis, 13th International Symposium, Proceedings, SAS 2006, Seoul, Korea, August 29-31, 2006 (2006)), 52-70 · Zbl 1225.68067
[17] Lev-Ami, T.; Sagiv, S., TVLA: a system for implementing static analyses, (Static Analysis, 7th International Symposium, Proceedings. Static Analysis, 7th International Symposium, Proceedings, SAS 2000, Santa Barbara, CA, USA, June 29-July 1, 2000 (2000)), 280-301 · Zbl 0966.68580
[18] Yahav, E.; Reps, T. W.; Sagiv, S.; Wilhelm, R., Verifying temporal heap properties specified via evolution logic, Log. J. IGPL, 14, 5, 755-783 (2006) · Zbl 1108.68077
[19] Distefano, D.; Katoen, J.-P.; Rensink, A., Safety and liveness in concurrent pointer programs, (de Boer, F. S.; Bonsangue, M. M.; Graf, S.; de Roever, W. P., FMCO. FMCO, Lecture Notes in Computer Science, vol. 4111 (2006), Springer: Springer Berlin, Heidelberg, Amsterdam, The Netherlands), 280-312 · Zbl 1196.68045
[20] Rieger, S., Verification of Pointer Programs (2009), RWTH Aachen University, Ph.D. thesis
[21] del Mar Gallardo, M.; Merino, P.; Sanán, D., Model checking dynamic memory allocation in operating systems, J. Automat. Reason., 42, 2-4, 229-264 (2009) · Zbl 1192.68147
[22] Holzmann, G. J., The SPIN Model Checker - Primer and Reference Manual (2004), Addison-Wesley
[23] Falke, S.; Merz, F.; Sinz, C., LLBMC: improved bounded model checking of C programs using LLVM, (Tools and Algorithms for the Construction and Analysis of Systems (2013), Springer), 623-626
[24] Ball, T.; Levin, V.; Rajamani, S. K., A decade of software model checking with SLAM, Commun. ACM, 54, 7, 68-76 (2011)
[25] Beyer, D.; Henzinger, T. A.; Jhala, R.; Majumdar, R., The software model checker blast, Int. J. Softw. Tools Technol. Transf., 9, 5-6, 505-525 (2007)
[26] Lu, X.; Duan, Z.; Tian, C., Extending PPTL for verifying heap evolution properties, arXiv preprint
[27] Duan, Z., An Extended Interval Temporal Logic and a Framing Technique for Temporal Logic Programming (1996), University of Newcastle upon Tyne, Ph.D. thesis
[28] Tian, C.; Duan, Z., Propositional projection temporal logic, Büchi automata and ω-regular expressions, (Agrawal, M.; Du, D.-Z.; Duan, Z.; Li, A., Theory and Applications of Models of Computation. Theory and Applications of Models of Computation, Lecture Notes in Computer Science, vol. 4978 (2008), Springer: Springer Xi’an, China), 47-58 · Zbl 1140.03305
[29] Duan, Z.; Yang, X.; Koutny, M., Framed temporal logic programming, Sci. Comput. Program., 70, 1, 31-61 (2008) · Zbl 1131.68036
[30] Duan, Z.; Tian, C., A unified model checking approach with projection temporal logic, (Liu, S.; Maibaum, T. S.E.; Araki, K., ICFEM. ICFEM, Lecture Notes in Computer Science, vol. 5256 (2008), Springer: Springer Berlin, Heidelberg, Kitakyushu-City, Japan), 167-186
[31] Zhang, N.; Duan, Z.; Tian, C., Model checking concurrent systems with MSVL, Sci. China Inf. Sci., 59, 11, Article 118101 pp. (2016)
[32] Zhang, N.; Duan, Z.; Tian, C., Extending MSVL with function calls, (Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, Proceedings. Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, Proceedings, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014 (2014)), 446-458
[33] Wang, X.; Duan, Z.; Zhao, L., Formalizing and implementing types in MSVL, (Structured Object-Oriented Formal Language and Method - Third International Workshop. Structured Object-Oriented Formal Language and Method - Third International Workshop, SOFL+MSVL 2013, Queenstown, New Zealand, October 29, 2013 (2013)), 62-75, Revised Selected Papers
[34] Brochenin, R.; Demri, S.; Lozes, E., On the almighty wand, Inform. and Comput., 211, 106-137 (2012) · Zbl 1262.03051
[35] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic with infinite models, Acta Inform., 45, 1, 43-78 (2008) · Zbl 1141.68039
[36] Tian, C.; Duan, Z., Complexity of propositional projection temporal logic with star, Math. Structures Comput. Sci., 19, 1, 73-100 (2009) · Zbl 1161.03008
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.