Generating Abstract Graph-Based Procedure Summaries for Pointer Programs
Generating Abstract Graph-Based Procedure Summaries for Pointer Programs
复制标题
为指针程序生成基于抽象图的过程摘要
DOI：
10.1007/978-3-319-09108-2_4
复制
发表时间：
2014
期刊：
影响因子：
2.2
通讯作者：
T. Noll
中科院分区：
文献类型：
--
作者：
Christina Jansen;T. Noll
对运行在堆上的指针操作程序进行自动分析和验证是一项具有挑战性的任务。它需要抽象技术来处理复杂的程序行为和来自动态数据结构和递归过程的无限状态空间。以前的工作表明，超边替换文法为定义和实现这种抽象提供了一个直观和通用的概念。
The automated analysis and verification of pointer-manipulating programs operating on a heap is a challenging task. It requires abstraction techniques for dealing with complex program behaviour and unbounded state spaces that arise from both dynamic data structures and recursive procedures. In previous work it was shown that hyperedge replacement grammars provide an intuitive and versatile concept for defining and implementing such abstractions.