一句话：提出以程序合成为统一机制的静态分析框架，并用受限二阶逻辑片段建模多种验证任务。
本文提出一个基于程序合成的统一静态分析器设计框架。作者识别出带受限量词的二阶逻辑片段，足以建模多种静态分析任务，包括安全性证明、缺陷发现、终止与非终止证明以及重构等。针对使用位向量的程序，他们将该片段在有限域上的判定过程实现为程序合成器。基于该框架实例化了终止性、非终止性、安全性、缺陷发现、超优化和重构等验证任务，并与各领域专用工具及通用合成器对比。实验表明其合成器性能具有竞争力。
In this article, we propose a unified framework for designing static analysers based on program synthesis . For this purpose, we identify a fragment of second-order logic with restricted quantification that is expressive enough to model numerous static analysis problems (e.g., safety proving, bug finding, termination and non-termination proving, refactoring). As our focus is on programs that use bit-vectors, we build a decision procedure for this fragment over finite domains in the form of a program synthesiser. We provide instantiations of our framework for solving a diverse range of program verification tasks such as termination, non-termination, safety and bug finding, superoptimisation, and refactoring. Our experimental results show that our program synthesiser compares positively with specialised tools in each area as well as with general-purpose synthesisers.
@article{paperbot320,
title = {Program Synthesis for Program Analysis},
author = {Cristina David and Pascal Kesseli and Daniel Kroening and Matt Lewis},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {40},
number = {2},
year = {2018},
doi = {10.1145/3174802}
}