Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps

Authors

  • Muhsin H. Atto Dept. of Computer Science, Faculty of Science, University of Zakho, Kurdistan Region, Iraq

DOI:

https://doi.org/10.25271/sjuoz.2021.9.1.778

Keywords:

Trees, Heaps, Graph Inclusion, Graph Matching, Software Verification

Abstract

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.

Author Biography

Muhsin H. Atto, Dept. of Computer Science, Faculty of Science, University of Zakho, Kurdistan Region, Iraq

Dept. of Computer Science, Faculty of Science, University of Zakho, Kurdistan Region, Iraq – (muhsin.atto@uoz.edu.krd)

References

Abdulla, P., Atto, M., Cederberg, J., and Ji, R. (2010). Automatic verification of dynamic data-dependent programs. LNCS, 5799:1–25.
Abdulla, P., Bouajjani, A., Cederberg, J., Haziza, F., Ji, R., and Rezine, A. (2008a). "shape analysis via monotonic abstraction". Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
Abdulla, P., Bouajjani, A., Cederberg, J., Haziza, F., and Rezine, A. (2008b). "monotonic abstraction for programs with dynamic memory heaps",lncs. volume 5123, pages 341–354.
Abdulla, P., Cederberg, J., and Vojnar, T. (2011). "monotonic abstraction for programs with multiply-linked structures",lncs. volume 6945, pages 125–138.
Abdulla, P., Delzanno, G., Henda, N., and Rezine, A. (2009). Monotonic abstraction: on efficient verification of parameterized systems. Int. J. Found. Comput. Sci., 20:779–801.
Asratian, A. S., Denley, T. M. J., and Häggkvist, R. (1998). Bipartite Graphs and Their Applications. USA.
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P. W., Wies, T., and Yang, H. (2007). Shape analysis forcomposite data structures. In Damm, W. and Hermanns, H., editors, Computer Aided Verification, pages 178–192, Berlin,Heidelberg. Springer Berlin Heidelberg.
Bouajjani, A. (2005). "regular model checking for programs with dynamic memory". 1:17–22.
Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., and Vojnar, T. (2006). "programs with lists are counter automata". In Ball, T. and Jones, R. B., editors, "Computer Aided Verification", pages 517–531, Berlin, Heidelberg. Springer Berlin Heidelberg.
Duan, R., Pettie, S., and Su, H.-H. (2018). Scaling algorithms for weighted matching in general graphs. ACM Trans. Algorithms, 14(1).
Gallardo, M.-d.-M., Merino, P., and Sanán, D. (2008). "model checking c programs with dynamic memory allocation". pages 219 – 226.
Giamblanco, N. and Anderson, J. (2019). "asap: Automatic sizing and partitioning for dynamic memory heaps in high-level synthesis", icfpt. pages 275–278.
Gotsman, A., Berdine, J., and Cook, B. (2006). Interprocedural shape analysis with separated heap abstractions. In Yi, K., editor, Static Analysis, pages 240–260, Berlin, Heidelberg.
Katrenic, J. and Semanisin, G. (2011). A generalization of hopcroft-karp algorithm for semi-matchings and covers in bipartite graphs. CoRR, abs/1103.1091.
Magill, S., Berdine, J., Clarke, E., and Cook, B. (2007). Arithmetic strengthening for shape analysis. In Nielson, H. R. and Filé, G., editors, Static Analysis, pages 419–436, Berlin, Heidelberg.
Valiente, G. (2005). Constrained tree inclusion. Journal of Discrete Algorithms, 3(2):431 – 447.
Wimmer, S. (2016). Timed automata. Archive of Formal Proofs.
Wimmer, S. and Lammich, P. (2018). Verified model checking of timed automata. In Beyer, D. and Huisman, M., editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 61–78, Cham. Springer International Publishing.

Downloads

Published

2021-03-30

How to Cite

Atto, M. H. (2021). Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps. Science Journal of University of Zakho, 9(1), 30–37. https://doi.org/10.25271/sjuoz.2021.9.1.778

Issue

Section

Science Journal of University of Zakho