Scholarlink

In this report, we provide our full set of results for the experimental evaluation of our formally verified, WTO-based dataflow solvers  [2]. We also detail useful information regarding our artifact [3] and evaluation setup. In particular, we validate experimentally that our implementation of Bourdoncle’s iteration strategies have acceptable performances in practice, when applied to the dataflow analyses used in the CompCert C verified compiler. Our experiments also help better understanding the differences between the solvers, their strengths and their weaknesses.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Formal Verification of WTO-based Dataflow Solvers

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年

查看全文
  • Roméo La Spina,
  • Delphine Demange,
  • Sandrine Blazy

摘要

In this report, we provide our full set of results for the experimental evaluation of our formally verified, WTO-based dataflow solvers  [2]. We also detail useful information regarding our artifact [3] and evaluation setup. In particular, we validate experimentally that our implementation of Bourdoncle’s iteration strategies have acceptable performances in practice, when applied to the dataflow analyses used in the CompCert C verified compiler. Our experiments also help better understanding the differences between the solvers, their strengths and their weaknesses.