Predator 形状分析器背后的算法细节

本章节是对会议论文《Predator：低级列表操作的字节精确验证》的扩展和修订版，集中于对 Predator 形状分析器算法细节的详细描述，该分析器基于抽象解释和符号内存图。Predator 特别适用于对使用低级指针操作来操作大小为无界的各种类型链表以及其他各种大小为有界的指针结构的顺序非递归 C 代码进行形式化分析和验证。该工具支持实用相关的指针算术、块操作、地址对齐或内存重新解释。我们介绍了该工具的整体架构，以及所选实现细节，并阐述了其扩展为所谓 Predator Hunting Party 的过程，后者利用多个并发运行的 Predator 分析器，每个分析器对其行为施加各种限制。提供了在 SV-COMP 竞赛中使用 Predator 的实验结果以及在我们自身基准测试中的结果。