3 ms·
It doesn’t surprise me at all that bugs were found in SMT Checker. I recently wrote a blog post on how Solidity’s model checker works, and stumbled across sever
by e79 6y ago
It doesn’t surprise me at all that bugs were found in SMT Checker. I recently wrote a blog post on how Solidity’s model checker works, and stumbled across several bugs while attempting to write simple example contracts. I didn’t even need a fuzzer :).
That area of the codebase is far from complete, which is why it is considered experimental and hidden behind a flag that you have to manually enable.
- pfdietz 6y agoOne of the distinguished papers at PLDI this year is on fuzzing for SMT solvers. People have been fuzzing these solves for years, but even now new approaches find new bugs. https://testsmt.github.io/papers/winterer-zhang-su-pldi20.pdf https://testsmt.github.io/papers/winterer-zhang-su-pldi20.pd...