3 ms·
High-Throughput, Formal-Methods-Assisted Fuzzing for LLVM [pdf]
- pfdietz 3y agoAssociated blog entry: https://blog.regehr.org/archives/2148 https://blog.regehr.org/archives/2148
- brookst 3y agoPaper is very confusing if the past year had trained your brain to skip the V in LLVM.
- deleted 3y ago[deleted]
- saagarjha 3y agoConsider getting a better model that doesn’t hallucinate like that.
- isaacfrond 3y agoAfter scanning the paper and blog post, I miss what formal methods they are using. Apparently they have a system that given two source code fragments can proof they are not equivalent. What are they using for that?
- quazar 3y agoFormal specification of LLVM and compile semantics to Z3, I would guess.
- boomanaiden154 3y agoPretty much this. It's called Alive2. https://dl.acm.org/doi/abs/10.1145/3453483.3454030 https://dl.acm.org/doi/abs/10.1145/3453483.3454030
- isaacfrond 3y agotnanks