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 lower false positive rates overall.
Thu 13 OctDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Technical Session 29 - AI for SE IIResearch Papers / Journal-first Papers at Ballroom C East Chair(s): Tim Menzies North Carolina State University | ||
16:00 20mResearch paper | Are Neural Bug Detectors Comparable to Software Developers on Variable Misuse Bugs? Research Papers Cedric Richter University of Oldenburg, Jan Haltermann University of Oldenburg, Marie-Christine Jakobs Technical University of Darmstadt, Felix Pauck Paderborn University, Germany, Stefan Schott Paderborn University, Heike Wehrheim University of Oldenburg DOI Pre-print Media Attached File Attached | ||
16:20 20mResearch paper | Learning Contract Invariants Using Reinforcement Learning Research Papers Junrui Liu University of California, Santa Barbara, Yanju Chen University of California at Santa Barbara, Bryan Tan Amazon Web Services, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara | ||
16:40 20mResearch paper | Compressing Pre-trained Models of Code into 3 MB Research Papers Jieke Shi Singapore Management University, Zhou Yang Singapore Management University, Bowen Xu School of Information Systems, Singapore Management University, Hong Jin Kang Singapore Management University, Singapore, David Lo Singapore Management University DOI Pre-print Media Attached | ||
17:00 20mResearch paper | A Transferable Time Series Forecasting Service using Deep Transformer model for Online SystemsVirtual Research Papers Tao Huang Tencent, Pengfei Chen Sun Yat-Sen University, Jingrun Zhang School of Data and Computer Science, Sun Yat-sen University, Ruipeng Li Tencent, Rui Wang Tencent | ||
17:20 20mPaper | The Weights can be Harmful: Pareto Search versus Weighted Search in Multi-Objective Search-Based Software EngineeringVirtual Journal-first Papers Pre-print | ||
17:40 20mResearch paper | Robust Learning of Deep Predictive Models from Noisy and Imbalanced Software Engineering DatasetsVirtual Research Papers Zhong Li Nanjing, Minxue Pan Nanjing University, Yu Pei Hong Kong Polytechnic University, Tian Zhang Nanjing University, Linzhang Wang Nanjing University, Xuandong Li Nanjing University |