paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Testing Dafny (experience paper)

测试 Dafny（经验论文）
ISSTA Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis2022匹配度 3/10 · 论文关注 Dafny 验证器与多后端编译器的模糊测试和差分测试，属于程序验证工具链质量保障，与形式化验证有间接关联；但未涉及 LLM/Agent 改进静态分析或验证、ML/Agent 程序静态分析、浮点程序分析或贝叶斯程序分析等画像核心方向。引用 15 inbox
Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamarić, Neha Rungta, Emina Torlak
测试、调试与修复程序验证
crossref: 2026-09-12

AI 速览

一句话：为 Dafny 验证器与多后端编译器构建首个模糊测试和差分测试框架，以发现工具链缺陷。

验证工具链被广泛用于证明关键软件系统的正确性，但工具链本身也可能存在缺陷，因此需要测试框架来增强对其结果的信心。受模糊测试在编译器和 SMT 求解器中发现缺陷的成功启发，本文介绍了首个面向 Dafny 的模糊测试与差分测试框架。Dafny 是一种高层编程语言，带有 Floyd-Hoare 风格的程序验证器，并提供到 C#、Java、Go 和 JavaScript 的编译器。该经验论文描述了如何将 fuzzing 与差分测试应用于这一验证和编译工具链，以检测其中潜在的错误，从而提升 Dafny 工具链的可靠性。

问题
验证工具链广泛用于证明关键软件正确性，但其自身可能含有缺陷，缺乏测试手段会削弱验证结果的可信度。
方法
受编译器和 SMT 求解器 fuzzing 成功启发，作者为 Dafny 构建首个模糊测试与差分测试框架。
评估
该框架面向 Dafny 的 Floyd-Hoare 风格验证器及其到 C#、Java、Go 和 JavaScript 的编译器进行测试，目标是发现工具链缺陷。
原文摘要（Abstract）

Verification toolchains are widely used to prove the correctness of critical software systems. To build confidence in their results, it is important to develop testing frameworks that help detect bugs in these toolchains. Inspired by the success of fuzzing in finding bugs in compilers and SMT solvers, we have built the first fuzzing and differential testing framework for Dafny, a high-level programming language with a Floyd-Hoare-style program verifier and compilers to C#, Java, Go, and Javascript.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot7401,
  title = {Testing Dafny (experience paper)},
  author = {Ahmed Irfan and Sorawee Porncharoenwase and Zvonimir Rakamarić and Neha Rungta and Emina Torlak},
  booktitle = {ISSTA},
  year = {2022},
  doi = {10.1145/3533767.3534382}
}