2026-07-26T11:36:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1559 2024-03-06T11:08:06Z ddc:004 open_access

Shape Analysis via Monotonic Abstraction Aziz Abdulla, Parosh Bouajjani, Ahmed Cederberg, Jonathan Haziza, Frédéric Ji, Ran Rezine, Ahmed Shape analysis Program verification Static analysis We propose a new formalism for reasoning about dynamic memory heaps, using monotonic abstraction and symbolic backward reachability analysis. We represent the heaps as graphs, and introduce an ordering on these graphs. This enables us to represent the violation of a given safety property as the reachability of a finitely representable set of bad graphs. We also describe how to symbolically compute the reachable states in the transition system induced by a program. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Parosh Aziz Abdulla and Ahmed Bouajjani and Jonathan Cederberg and Frédéric Haziza and Ran Ji and Ahmed Rezine 2008 Is Part Of Dagstuhl Seminar Proceedings, Volume 8171, Beyond the Finite: New Challenges in Verification and Semistructured Data (2008) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.08171.3 urn:nbn:de:0030-drops-15590 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08171.3 eng https://creativecommons.org/licenses/by/4.0/legalcode