Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps
Programs that manipulate heaps such as singlylinked lists, doublylinked lists, skiplists, and treesare ubiquitous, and hence ensuring their correctness is of utmost importance. Analysing correctness properties for such programs is not trivial since they induce dynamic data structures, le...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Zakho
2021-03-01
|
| Series: | Science Journal of University of Zakho |
| Subjects: | |
| Online Access: | http://sjuoz.uoz.edu.krd/index.php/sjuoz/article/view/778 |
| _version_ | 1819240844206538752 |
|---|---|
| author | Muhsin H. Atto |
| author_facet | Muhsin H. Atto |
| author_sort | Muhsin H. Atto |
| collection | DOAJ |
| description | Programs that manipulate heaps such as singlylinked lists, doublylinked lists, skiplists, and treesare ubiquitous, and hence ensuring their correctness is of utmost importance. Analysing correctness properties for such programs is not trivial since they induce dynamic data structures, leading to unbounded state spaces with intricate patterns. One approach that has been adopted to tackle this problem is the use of symbolic searching techniques. The state space is encoded using graphs where the nodes represent memory cells, and the edges represent pointers between the cells. It is necessary to prune the search to avoid generating massive numbers of graphs, thus making the procedure unpractical. Pruning strategies are defined based on operations such as graph matching and inclusion. In this paper, a set of algorithms for performing these operations are presented. It is demonstrated that the proposed algorithms can handle typical graphs that arise in the verification of heap manipulating programs. |
| first_indexed | 2024-12-23T14:14:28Z |
| format | Article |
| id | doaj.art-e5b2432d919d4cee9134eab5397ab27d |
| institution | Directory Open Access Journal |
| issn | 2663-628X 2663-6298 |
| language | English |
| last_indexed | 2024-12-23T14:14:28Z |
| publishDate | 2021-03-01 |
| publisher | University of Zakho |
| record_format | Article |
| series | Science Journal of University of Zakho |
| spelling | doaj.art-e5b2432d919d4cee9134eab5397ab27d2022-12-21T17:43:58ZengUniversity of ZakhoScience Journal of University of Zakho2663-628X2663-62982021-03-019110.25271/sjuoz.2021.9.1.778Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked HeapsMuhsin H. Atto0Dept. of Computer Science, Faculty of Science, University of Zakho, Kurdistan Region, IraqPrograms that manipulate heaps such as singlylinked lists, doublylinked lists, skiplists, and treesare ubiquitous, and hence ensuring their correctness is of utmost importance. Analysing correctness properties for such programs is not trivial since they induce dynamic data structures, leading to unbounded state spaces with intricate patterns. One approach that has been adopted to tackle this problem is the use of symbolic searching techniques. The state space is encoded using graphs where the nodes represent memory cells, and the edges represent pointers between the cells. It is necessary to prune the search to avoid generating massive numbers of graphs, thus making the procedure unpractical. Pruning strategies are defined based on operations such as graph matching and inclusion. In this paper, a set of algorithms for performing these operations are presented. It is demonstrated that the proposed algorithms can handle typical graphs that arise in the verification of heap manipulating programs.http://sjuoz.uoz.edu.krd/index.php/sjuoz/article/view/778TreesHeapsGraph InclusionGraph MatchingSoftware Verification |
| spellingShingle | Muhsin H. Atto Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps Science Journal of University of Zakho Trees Heaps Graph Inclusion Graph Matching Software Verification |
| title | Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps |
| title_full | Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps |
| title_fullStr | Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps |
| title_full_unstemmed | Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps |
| title_short | Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps |
| title_sort | graph inclusion and matching algorithms for programs manipulating singly linked heaps |
| topic | Trees Heaps Graph Inclusion Graph Matching Software Verification |
| url | http://sjuoz.uoz.edu.krd/index.php/sjuoz/article/view/778 |
| work_keys_str_mv | AT muhsinhatto graphinclusionandmatchingalgorithmsforprogramsmanipulatingsinglylinkedheaps |