[Solidity] thoughts - Githubissues

ChenfengWei0 / esbmc

The efficient SMT-based bounded model checker

http://esbmc.org/

Other

0 stars 1 forks source link

[Solidity] thoughts #6

Open ChenfengWei0 opened 1 year ago

ChenfengWei0 commented 1 year ago

what are the bugs that esbmc can verify? what kinds of bugs cannot

ChenfengWei0 commented 1 year ago

challenge: sol => c

ChenfengWei0 commented 1 year ago

database categorize

ChenfengWei0 commented 1 year ago

There is a trend to .. consist of not only verification, but static analysis, and fuzz testing. Do we still need pattern-base checking?

ChenfengWei0 commented 1 year ago

BMC checker in Solidity needs some special function. E.g. report unreachable code( this means the transaction that will never happen.) Or assume sth works

ChenfengWei0 commented 1 year ago

Can reentryattack be verified?

ChenfengWei0 commented 1 year ago

Gas verification