一句话：提出用 Flix 语言实现静态分析，从语言层面保障不动点计算安全终止且分析结果可靠。
静态分析工具被广泛用于缺陷查找、构建、编译、调试、IDE 和重构，但其实现本身复杂：不动点计算必须收敛、终止并给出确定结果（安全性），计算结果还必须过近似程序的真实行为（可靠性）。本文以 Flix 语言为依托，探讨如何安全且可靠地实现程序分析，使分析实现者不必独自承担对分析结果可信度的论证。论文强调，如果分析语言能保证固定点计算和过近似语义，那么“谁来监督监督者”的问题就可在语言层面得到回应。摘要未给出具体实验评估。
Program development tools such as bug finders, build automation tools, compilers, debuggers, integrated development environments, and refactoring tools increasingly rely on static analysis techniques to reason about program behavior. Implementing such static analysis tools is a complex and difficult task with concerns about safety and soundness. Safety guarantees that the fixed point computation -- inherent in most static analyses -- converges and ultimately terminates with a deterministic result. Soundness guarantees that the computed result over-approximates the concrete behavior of the program under analysis. But how do we know if we can trust the result of the static analysis itself? Who will guard the guards?
DOI 原文 ·
@inproceedings{paperbot4837,
title = {Safe and sound program analysis with Flix},
author = {Magnus Madsen and Ondřej Lhoták},
booktitle = {ISSTA},
year = {2018},
doi = {10.1145/3213846.3213847}
}