使用控制流重构改进参数化布尔方程系统的静态分析
Improved Static Analysis of Parameterised Boolean Equation Systems using Control Flow Reconstruction
AI总结：
提出一种基于控制流重构的静态分析技术，通过检测并消除不活跃参数来缓解参数化布尔方程系统的组合爆炸，并定义近似分析以避免控制流图构建的指数级爆炸，案例研究验证了其有效性。
摘要：
我们提出了一种可靠的静态分析技术，用于应对参数化布尔方程系统（PBESs）的组合爆炸问题。这些系统本质上是一阶逻辑公式上的相互递归不动点方程组。我们的方法通过分析PBES的控制流图来检测不活跃的参数，并随后消除这些参数。我们表明，构建用于分析的控制流图的朴素方法可能遭受指数级爆炸，因此我们定义了一种避免此问题的近似分析。我们技术的有效性通过多个案例研究进行了评估。
英文摘要：
We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order logic formulae. Our method detects parameters that are not live by analysing a control flow graph of a PBES, and it subsequently eliminates such parameters. We show that a naive approach to constructing a control flow graph, needed for the analysis, may suffer from an exponential blow-up, and we define an approximate analysis that avoids this problem. The effectiveness of our techniques is evaluated using a number of case studies.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
