Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
作者： Cristiano Calcagno , Dino Distefano , Peter W. O’Hearn , Hongseok Yang
DOI: 10.1007/11823230_13
关键词: Dynamic memory management 、 Separation logic 、 Abstract interpretation 、 Heap (data structure) 、 Reachability 、 Logical programming 、 Pointer (computer programming) 、 Symbolic execution 、 Escape analysis 、 Arithmetic 、 Memory model 、 Computer science 、 Algorithm 、 Random access memory 、 Free list 、 Pointer analysis
摘要: Previous shape analysis algorithms use a memory model where the heap is composed of discrete nodes that can be accessed only via access paths built from variables and field names, an assumption violated by pointer arithmetic. In this paper we show how removed, arithmetic embraced, using based on separation logic. We describe abstract domain whose elements are certain logic formulae, abstraction mechanism automatically transits between low-level RAM view higher, fictional, abstracts representation multiword linked-lists as configurations RAM. A widening operator used to accelerate analysis. report experimental results obtained running our number classic for dynamic management.
springer.com
sci-hub.st 参考文章(40)
Bjarne Stroustrup, The C++ programming language (2nd ed.) Addison-Wesley Longman Publishing Co., Inc.. ,(1991)
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
Dino Distefano, Peter W. O’Hearn, Hongseok Yang, A local shape analysis based on separation logic tools and algorithms for construction and analysis of systems. ,vol. 3920, pp. 287- 302 ,(2006) , 10.1007/11691372_19
Roman Manevich, E. Yahav, G. Ramalingam, Mooly Sagiv, Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists Lecture Notes in Computer Science. pp. 181- 198 ,(2005) , 10.1007/978-3-540-30579-8_13
Ittai Balaban, Amir Pnueli, Lenore D. Zuck, Shape Analysis by Predicate Abstraction Lecture Notes in Computer Science. pp. 164- 180 ,(2005) , 10.1007/978-3-540-30579-8_12
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Gogul Balakrishnan, Thomas Reps, Recency-Abstraction for Heap-Allocated Storage Static Analysis. pp. 221- 239 ,(2006) , 10.1007/11823230_15
Ahmed Bouajjani, Peter Habermehl, Pierre Moro, Tomáš Vojnar, Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking Tools and Algorithms for the Construction and Analysis of Systems. pp. 13- 29 ,(2005) , 10.1007/978-3-540-31980-1_2
Eric A. Brewer, Alexander Aiken, David A. Wagner, Jeffrey S. Foster, A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. network and distributed system security symposium. ,(2000)
Nicolas Marti, Reynald Affeldt, Akinori Yonezawa, Formal verification of the heap manager of an operating system using separation logic formal methods. pp. 400- 419 ,(2006) , 10.1007/11901433_22