Hello, I'm Yeonghun and this issue is the responses for the questions I got in the presentation.
First, the professor's question was,
"Why are the testcases said to be verified even if they have non-zero alarms?"
The verified check mark does not mean that a testcase is bug-free, but it means that a verifier(e.g., VERISMART) can pinpoint all vulnerable locations in the sourcecode.
and for the Taeeun's second question,
"Why did Zeus fail to verify all testcases even the testcases are the ones in its paper?"
To put it briefly, a verifier is said to fail to verify a testcase if it has any false positives.
I'll quote the explanation in the paper as follows,
However, the public data was not detailed enough to accurately interprete as the ZEUS authors classify each benchmark contract simply as ‘safe’ or ‘unsafe’ without specific alarm information such as line numbers. The only objective information we could obtain from the data [28] was the fact that ZEUS produces some (nonzero) number of false (arithmetic-overflow) alarms on 40 contracts, and we decided to use those in our evaluation.
...
The column
Verified indicates whether each tool detected all bugs without
false positives (✓: success, ✗: failure).
Hello, I'm Yeonghun and this issue is the responses for the questions I got in the presentation.
First, the professor's question was,
The verified check mark does not mean that a testcase is bug-free, but it means that a verifier(e.g., VERISMART) can pinpoint all vulnerable locations in the sourcecode.
and for the Taeeun's second question,
To put it briefly, a verifier is said to fail to verify a testcase if it has any false positives.
I'll quote the explanation in the paper as follows,
Thank you for the questions!