SPARTA

SPARTA

SPARTA 是一套软件组件库,专门用于基于抽象解释理论构建高性能静态分析器。

摘要解释

抽象解释 是一种语义近似理论,为静态程序分析器的设计提供了基础框架。遵循抽象解释方法构建的静态分析器在数学上是可靠的,即它们计算的语义信息在所有可能的执行上下文中都得以保证。此外,这些分析器能够推断程序的复杂属性,其表达能力可以精细调整,以控制分析时间。基于抽象解释的静态分析器通常用于进行航空航天工业中的飞行软件的形式验证。

为什么是 SPARTA？从头构建基于抽象解释的工业级静态分析工具是一项艰巨的任务，需要该领域的专家的关注。SPARTA 的目的是通过提供一组具有简单 API、性能高且可轻松组装的软件组件，大幅简化抽象解释的工程工作，从而构建出具有生产级质量的静态分析器。通过封装抽象解释的复杂实现细节，SPARTA 使工具开发者能够专注于分析设计的三个基本轴：

• **语义：**需要分析的程序属性（数值变量的范围、别名关系等）
• **分区：**分析属性的粒度（过程内、过程间、上下文敏感等）
• **抽象：**程序属性的表示（符号、区间、别名图等）