Experiment 1-RQ1

The table above shows the complete results for Invariant Effectiveness Evaluation(Experiment 1-RQ1)

The numbers in this table represent the ratios of non-exploit transactions blocked by corresponding invariant guard(False Positive Rates)
Grey cells indicate the exploit transaction is blocked by corresponding invariant guard(True Positives)
There are  three  reasons that one invariant is not available for one benchmark:

1.  Symbol - represents that the invariant is by nature not applicable to the benchmark contract. For example, if a contract does not have a member variable totalSupply, then the invariant TSU(total supply upperbound) is by nature not applicable. 

2.  Symbol x represents that the transactions in the training set violate the invariant. It represents normal users will violate this invariant, therefore this invariant does not stand for normal users' behaviors. Thus, the invariant is not applicable.  

3.  Symbol Ø represents the transactions in the training set do not have enough data points. For example, for invariant SM(isSenderManager), the manager addresses must be learnt from training set to concretize this invariant. Since we define there should be 2-5 managers for each function, if all functions of target transactions have more than 5 distinct msg.senders or have only 0-1 distinct msg.senders, no concretized SM invariants are learnt by trace2inv. Thus, the invariant is not applicable.