hi everyone!
I want to listen how ISLE rules are maintained in terms of its correctness.
Is there anyone working on applying techniques such as fuzz-testing, translation validation or formal verification to ISLE rules?
thank you!
You may be interested in this talk, which I gave recently (two weeks ago) and which describes exactly this topic!
(slides here)
and you'll likely be interested in our paper here about SMT-based verification of lowering rules in ISLE; and my blog post here about translation validation in the register allocator
The ASPLOS paper project is still ongoing work, and we hope to have more at some point. I'm also continuing to push proof-carrying code forward in the background (as I described in that talk)
as far as fuzzing, it is done pervasively in the Cranelift+Wasmtime codebase; take a look at our fuzz-targets here
I'll take a look into those, thank you!
for a high level overview, there is also https://bytecodealliance.org/articles/security-and-correctness-in-wasmtime
Last updated: Feb 27 2025 at 23:03 UTC