  At present, millions of Ethereum smart contracts are created per year and
attract financially motivated attackers. However, existing analyzers do not
meet the need to precisely analyze the financial security of large numbers of
contracts. In this paper, we propose and implement FASVERIF, an automated
analyzer for fine-grained analysis of smart contracts' financial security. On
the one hand, FASVERIF automatically generates models to be verified against
security properties of smart contracts. On the other hand, our analyzer
automatically generates the security properties, which is different from
existing formal verifiers for smart contracts. As a result, FASVERIF can
automatically process source code of smart contracts, and uses formal methods
whenever possible to simultaneously maximize its accuracy.
  We evaluate FASVERIF on a vulnerabilities dataset by comparing it with other
automatic tools. Our evaluation shows that FASVERIF greatly outperforms the
representative tools using different technologies, with respect to accuracy and
coverage of types of vulnerabilities.
