The Top-Down Solver—An Exercise in $$\text {A}^{2}$$I
Intelligent systems reference library(2023)
摘要
The top-down solver TD is a convenient local generic fixpoint engine which is at the heart of static analysis frameworks such as Ciao and Goblint. Here, we show how Patrick Cousot’s idea of applying analysis to the analyzer itself allows to derive advanced versions of TD from a recursive descent fixpoint algorithm. A run of that fixpoint algorithm provides us with a trace whose dynamic analysis allows not only to identify semantic dependencies between unknowns on-the-fly, but also to choose appropriate widening/narrowing points. It is thus not only the sequence of iterates for individual unknowns which is taken into account, but the global trace of the fixpoint algorithm itself.
更多查看译文
关键词
solver—an,top-down
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要