Write a Blog >>

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 Oct

Displayed 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
20m
Research 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
20m
Paper
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
20m
Research paper
Learning to Synthesize Relational Invariants
Research Papers
Jingbo Wang University of Southern California, Chao Wang USC
17:00
10m
Demonstration
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
20m
Research 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
10m
Demonstration
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
20m
Research paper
Studying and Understanding the Tradeoffs Between Generality and Reduction in Software DebloatingVirtual
Research Papers
Qi Xin Wuhan University, Qirun Zhang Georgia Institute of Technology, Alessandro Orso Georgia Tech