We propose a method for synthesizing invariants that can help verify relational properties over two programs or two different executions of a program. Applications of such invariants include verifying functional equivalence, non-interference security, and continuity properties. Our method generates invariant candidates using syntax guided synthesis (SyGuS) and then filters them using an SMT-solver based verifier, to ensure they are both inductive invariants and sufficient for verifying the property at hand. To improve performance, we propose two learning based techniques: a logical reasoning (LR) technique to determine which part of the search space can be pruned away, and a reinforcement learning (RL) technique to determine which part of the search space to prioritize. Our experiments on a diverse set of relational verification benchmarks show that our learning based techniques can drastically reduce the search space and, as a result, they allow our method to generate invariants of a higher quality in much shorter time than state-of-the-art invariant synthesis techniques.
Thu 13 OctDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Technical Session 31 - Code Similarities and RefactoringResearch Papers / Tool Demonstrations / Journal-first Papers at Banquet A Chair(s): Hua Ming Oakland University | ||
16:00 20mResearch paper | Reformulator: Automated Refactoring of the N+1 Problem in Database-Backed Applications Research Papers Alexi Turcotte Northeastern University, Mark W. Aldrich Tufts University, Frank Tip Northeastern University | ||
16:20 20mPaper | How Software Refactoring Impacts Execution Time Journal-first Papers Luca Traini University of L'Aquila, Daniele Di Pompeo University of L'Aquila, Michele Tucci Charles University, Bin Lin Radboud University, Simone Scalabrino University of Molise, Gabriele Bavota Software Institute, USI Università della Svizzera italiana, Michele Lanza Software Institute - USI, Lugano, Rocco Oliveto University of Molise, Vittorio Cortellessa University of L'Aquila Link to publication DOI Authorizer link | ||
16:40 20mResearch paper | Learning to Synthesize Relational Invariants Research Papers | ||
17:00 10mDemonstration | AntiCopyPaster: Extracting Code Duplicates As Soon As They Are Introduced in the IDE Tool Demonstrations Eman Abdullah AlOmar Stevens Institute of Technology, Anton Ivanov HSE University, Zarina Kurbatova JetBrains Research, Yaroslav Golubev JetBrains Research, Mohamed Wiem Mkaouer Rochester Institute of Technology, Ali Ouni ETS Montreal, University of Quebec, Timofey Bryksin JetBrains Research, Le Nguyen Rochester Institute of Technology, Amit Kini Rochester Institute of Technology, Aditya Thakur Rochester Institute of Technology DOI Pre-print | ||
17:10 20mResearch paper | TreeCen: Building Tree Graph for Scalable Semantic Code Clone DetectionVirtual Research Papers Yutao Hu Huazhong University of Science and Technology, Deqing Zou Huazhong University of Science and Technology, Junru Peng Xidian University, Yueming Wu Nanyang Technological University, Junjie Shan KTH Royal Institute of Technology, Hai Jin Huazhong University of Science and Technology | ||
17:30 10mDemonstration | Trimmer: Context-Specific Code ReductionVirtual Tool Demonstrations Aatira Anum Ahmad Lahore University of Management Sciences, Mubashir Anwar University of Illinois Urbana-Champaign, Hashim Sharif University of Illinois at Urbana-Champaign, Ashish Gehani SRI, Fareed Zaffar Lahore University of Management Sciences | ||
17:40 20mResearch paper | Studying and Understanding the Tradeoffs Between Generality and Reduction in Software DebloatingVirtual Research Papers |