模块化分析数值属性：基于抽象解释的方法

"HAL多学科开放获取存档包含了一篇由Rémy Boutonnet撰写的博士论文，主题是通过抽象解释进行数值属性的模块化分析。这篇论文属于数据结构与算法领域，作者在格勒诺布尔阿尔卑斯大学完成，专业为计算机科学。论文于2020年3月9日公开支持，并由尼古拉斯·哈尔布瓦克斯指导。评审委员会包括多位知名学者和研究人员。" 这篇博士论文的核心内容聚焦于程序验证和分析，特别是在安全关键系统中的应用。在这样的系统中，软件错误可能导致严重后果，因此对程序进行验证和分析以确保其符合规范并消除运行时错误至关重要。论文采用抽象解释这一静态程序分析方法，该方法能够近似地计算出程序的所有可达状态。通过这种方式，可以识别和表达程序的不变性属性，这些属性由抽象域的元素来表示。 抽象解释是一种形式验证技术，它将程序的行为映射到一个更简单的、通常离散的抽象域中，以便于分析。在模块化分析中，程序的不同部分被独立处理，然后整合结果以获得整体的理解。这种方法有助于处理大型复杂程序，使得分析更具可扩展性和效率。 论文可能详细探讨了如何构建和使用抽象域，以及如何推断和验证数值属性。可能还涉及了如何利用抽象解释来检测和预防潜在的错误，如内存泄漏、溢出或竞态条件。此外，作者可能讨论了如何将这种分析应用于实际的软件工程实践中，以及如何将模块化策略应用于不同的软件组件。 通过Rémy Boutonnet的工作，读者可以深入了解如何利用抽象解释技术来提高软件的安全性和可靠性，这对于软件开发和维护具有重要价值。这篇论文不仅是学术研究的贡献，也是实践指导，可能包含了一系列的案例研究和实验结果，证明了所提出方法的有效性。