Formal Verification of WTO-based Dataflow Solvers - Artifact Experience Report

Abstract

Abstract 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.