大型安全关键软件的静态分析器
A Static Analyzer for Large Safety-Critical Software
摘要：
我们表明，抽象的解释为基础的静态程序分析，可以有效和精确到足以正式验证一个家庭的大型程序很少或没有假警报的一类属性。这是通过通用静态分析器的改进以及最终用户通过参数化对该系列的特定程序进行调整来实现的。这是适用于在机器级的定期同步安全关键嵌入式软件的数据操作操作的可靠性的证明。主要的新颖性是静态分析器的设计原理，通过参数化进行细化和自适应，对表达式进行符号操作以提高抽象传递函数的精度，八边形，椭圆形和决策树抽象域，所有这些都具有浮点计算中舍入错误的良好处理，扩展策略（具有阈值，延迟）和参数的自动确定（参数化包装）。
英文摘要：
We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software. The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization, the symbolic manipulation of expressions to improve the precision of abstract transfer functions, the octagon, ellipsoid, and decision tree abstract domains, all with sound handling of rounding errors in floating point computations, widening strategies (with thresholds, delayed) and the automatic determination of the parameters (parametrized packing).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
