Shape Analysis via Monotonic Abstraction

Beyond the Finite: New Challenges in Verification and Semistructured Data

计算机科学;物理学

Parosh Aziz Abdulla1 ; Ahmed Bouajjani2 ; Jonathan Cederberg1

PID  :  81934

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

We propose a new formalism for reasoning about dynamicmemory heaps, using monotonic abstraction and symbolic backward reach ability analysis. We represent the heaps as graphs, and introduce an or dering 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