@INPROCEEDINGS{ase22-cider,
  title     = "Learning Contract Invariants Using Reinforcement Learning",
  booktitle = "Proceedings of the 37th {IEEE/ACM} International Conference on
               Automated Software Engineering",
  author    = "Liu, Junrui and Chen, Yanju and Tan, Bryan and Dillig, Isil and
               Feng, Yu",
  abstract  = "Due to the popularity of smart contracts in the modern financial
               ecosystem, there has been growing interest in formally verifying
               their correctness and security properties. Most existing
               techniques in this space focus on common vulnerabilities like
               arithmetic overflows and perform verification by leveraging
               contract invariants (i.e., logical formulas hold at transaction
               boundaries). In this paper, we propose a new technique, based on
               deep reinforcement learning, for automatically learning contract
               invariants that are useful for proving arithmetic safety. Our
               method incorporates an off-line training phase in which the
               verifier uses its own verification attempts to learn a policy
               for contract invariant generation. This learned (neural) policy
               is then used at verification time to predict likely invariants
               that are also useful for proving arithmetic safety. We
               implemented this idea in a tool called Cider and incorporated it
               into an existing verifier (based on refinement type checking)
               for proving arithmetic safety. Our evaluation shows that Cider
               improves both the quality of the inferred invariants as well as
               inference time, leading to faster verification and hardened
               contracts with fewer run-time assertions.",
  publisher = "Association for Computing Machinery",
  series    = "ASE '22",
  year      =  2023,
  address   = "New York, NY, USA",
  location  = "Rochester, MI, USA"
}