3
votes
Accepted
Symbolic Execution vs Fuzz Testing - What's the difference?
Summary
Fuzzing & Symbolic execution accomplish similar goals of finding cases where code breaks, but have tradeoffs in speed vs. precision, and take very different approaches.
Fuzzing: Much ...
- 12.4k
2
votes
Accepted
Is the solidity built-in SMT Checker a form of symbolic execution?
Yes. It is.
Symbolic Execution Primer
Symbolic Execution is a means of analyzing a program to determine what inputs cause each part of a program to execute. It will convert the program to a symbolic ...
- 12.4k
2
votes
Accepted
Halmos counterexamples not the actual counterexamples
Halmos finds list a single counterexample for each path it finds an issue, it doesn't list every possible counterexample (this could potentially be a lot of counterexamples.
So if you're looking to ...
- 12.4k
2
votes
Accepted
What is a minimal symbolic execution example?
When we look at this function, we can easily see two paths this function can take.
a < 2^256, a = a + 1, function returns
a == 2^256, a = a + 1 overflows, function reverts
We can turn these into ...
- 12.4k
1
vote
What's the difference between a SAT Solver and a SMT solver?
SAT solvers are used for Boolean formulas while SMT solvers can handle formulas that involve multiple theories. Both can be used to verify Solidity code, but SMT solvers are more powerful and can ...
- 11
1
vote
Accepted
Maat: RuntimeError: LoaderLIEF::parse_binary(): Couldn't parse file './myFile.out'
OS.LINUX won't work on a macOS. You'll have to run your code on a linux machine.
- 12.4k
Only top scored, non community-wiki answers of a minimum length are eligible