Automated Verification of Monotonic Data Structure Traversals in C
a year ago
- #programming
- #C
- #verification
- 现实世界的C代码中常见定制化数据结构操作。
- 单调数据结构遍历(MDSTs)会单调地迭代结构，例如strlen或二叉搜索树插入操作。
- Shrinker是用于C语言MDST的新型自动化验证工具，采用替罪羊规模下降分析法。
- 替罪羊规模下降技术利用原始输入与'缩减'输入之间的相似执行轨迹。
- 新基准测试集包含100多个实例，证明了主流C代码库中MDST的正确性、等价性和内存安全性。
- 在验证单调字符串和列表遍历方面，Shrinker性能优于最先进的工具。