Graph Inclusion and Matching Algorithms for Programs Manipulating Singly linked Heaps
DOI:
https://doi.org/10.25271/sjuoz.2021.9.1.778Keywords:
Trees, Heaps, Graph Inclusion, Graph Matching, Software VerificationAbstract
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.
References
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
How to Cite
Issue
Section
License
Authors who publish with this journal agree to the following terms:
- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License [CC BY-NC-SA 4.0] that allows others to share the work with an acknowledgment of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work, with an acknowledgment of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online.
