Synthesizing Program-Specific Static Analyses
Synthesizing Program-Specific Static Analyses
复制标题
综合特定于程序的静态分析
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Colin S. Gordon
中科院分区：
文献类型：
--
作者：
Colin S. Gordon
设计静态分析通常是一项艰巨的任务，需要程序分析和程序分析领域的丰富专业知识以及大量的开发资源。因此，大多数程序都会分析普遍感兴趣的目标属性（例如，不存在空指针取消引用）或几乎如此（例如，无死锁）。然而，许多从静态检查中受益的有趣的程序属性特定于单个程序，或者有时是使用特定库的程序。让程序分析和验证专家来解决这些问题是不切实际的。
相反，我们建议在类型限定符系统和效果系统等易于理解的领域内进行基于示例的程序分析综合。这些系统防止的问题类别背后的动态行为对应于缺乏静态分析专业知识的开发人员可以轻松提供的示例（数据流路径或堆栈跟踪）。
Designing a static analysis is generally a substantial undertaking, requiring significant expertise in both program analysis and the domain of the program analysis, and significant development resources. As a result, most program analyses target properties that are universallly of interest (e.g., absence of null pointer dereference) or nearly so (e.g., deadlock freedom). However, many interesting program properties that would benefit from static checking are specific to individual programs, or sometimes programs utilizing a certain library. It is impractical to devote program analysis and verification experts to these problems.
We propose instead to work on example-based synthesis of program analyses within well-understood domains like type qualifier systems and effect systems. The dynamic behaviors behind the classes of problems these systems prevent correspond to examples that developers who lack expertise in static analysis can readily provide (data flow paths, or stack traces).