Model checking recursive programs interacting via the heap

被引:1
作者
Asavoae, I. M. [2 ]
de Boer, F. [1 ,3 ]
Bonsangue, M. M. [1 ,3 ]
Lucanu, D. [2 ]
Rot, J. [1 ,3 ]
机构
[1] Leiden Inst Adv Comp Sci, Leiden, Netherlands
[2] Alexandru Ioan Cuza Univ, Fac Comp Sci, Iasi, Romania
[3] Ctr Wiskunde & Informat, Amsterdam, Netherlands
关键词
Heap manipulation; Pushdown system; Object-oriented program semantics; Model checking; VERIFICATION; AUTOMATA;
D O I
10.1016/j.scico.2014.09.009
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive procedures and local variables, the interactions of a program with the heap can become rather complex, as an unbounded number of objects can be allocated either on the call stack using local variables, or, anonymously, on the heap using reference fields. As such, a static analysis for recursive programs with dynamic manipulation of the heap is, in general, undecidable. In this paper we study the verification of recursive programs with unbounded allocation of objects, in a simple imperative language with heap manipulation. We present a semantics for this language which is improved w.r.t. heap allocation, using an abstraction that is precise (i.e., bisimilar with the standard/concrete semantics). For any program with a bounded visible heap, meaning that the number of objects reachable from variables at any point of execution is bounded, this abstraction is a finitary representation of its behaviour, even though an unbounded number of objects can appear in the state. As a consequence, for such programs model checking is decidable. Finally, we introduce a specification language for heap-properties, and we discuss model checking of heap invariant properties against heap-manipulating programs. (C) 2014 Published by Elsevier B.V.
引用
收藏
页码:61 / 83
页数:23
相关论文
共 36 条
[1]  
[Anonymous], 2002, PhD thesis
[2]  
Asavoae I.M., 2013, LNCS, V7841, P59
[3]  
Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[4]  
Berdine J, 2004, LECT NOTES COMPUT SC, V3328, P97
[5]  
Biere Armin, 2003, ADV COMPUT, V58, P118, DOI DOI 10.1016/S0065-2458(03)58003-2
[6]  
Bonsangue M, 2011, LECT NOTES COMPUT SC, V6527, P226, DOI 10.1007/978-3-642-19829-8_15
[7]  
Bouajjani A, 1997, LECT NOTES COMPUT SC, V1243, P135
[8]  
Bouajjani A, 2007, LECT NOTES COMPUT SC, V4590, P207
[9]   DERIVATIVES OF REGULAR EXPRESSIONS [J].
BRZOZOWSKI, JA .
JOURNAL OF THE ACM, 1964, 11 (04) :481-&
[10]   Symmetries, local names and dynamic (de)-allocation of names [J].
Ciancia, Vincenzo ;
Montanari, Ugo .
INFORMATION AND COMPUTATION, 2010, 208 (12) :1349-1367