Write a Blog >>
Thu 12 Nov 2020 08:35 - 08:36 at Virtual room 1 - Analysis 4

Loop invariant generation has long been a challenging problem. Black-box learning has recently emerged as a promising method for inferring loop invariants. However, the performance depends heavily on the quality of collected examples. In many cases, only after tens or even hundreds of constraint queries, can a feasible invariant be successfully inferred.

To reduce the gigantic number of constraint queries and improve the performance of black-box learning, we introduce interval counterexamples into the learning framework. Each interval counterexample represents a set of counterexamples from constraint solvers. We propose three different generalization techniques to compute interval counterexamples. The existing decision tree algorithm is also improved to adapt interval counterexamples. We evaluate our techniques and report over $40%$ improvement on learning rounds and verification time over the state-of-the-art approach.

Thu 12 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change

08:30 - 09:00: Analysis 4Paper Presentations / Research Papers at Virtual room 1
08:30 - 08:32
Talk
Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization
Research Papers
Dirk BeyerLMU Munich, Germany, Karlheinz FriedbergerLMU Munich, Germany
DOI Pre-print Media Attached
08:33 - 08:34
Talk
Inherent Vacuity for GR(1) Specifications
Research Papers
Shahar MaozTel Aviv University, Israel, Rafi ShalomTel Aviv University, Israel
DOI
08:35 - 08:36
Talk
Interval Counterexamples for Loop Invariant Learning
Research Papers
Rongchen XuTsinghua University, China, Fei HeTsinghua University, Bow-Yaw WangAcademia Sinica
DOI
08:37 - 08:38
Talk
Modular Collaborative Program Analysis in OPAL
Research Papers
Dominik HelmTU Darmstadt, Germany, Florian K├╝blerTU Darmstadt, Germany, Michael ReifTU Darmstadt, Germany, Michael EichbergTU Darmstadt, Germany, Mira MeziniTU Darmstadt, Germany
DOI
08:39 - 08:40
Talk
Past-Sensitive Pointer Analysis for Symbolic Execution
Research Papers
David TrabishTel Aviv University, Israel, Timotej KapusImperial College London, UK, Noam RinetzkyTel Aviv University, Cristian CadarImperial College London, UK
DOI Pre-print Media Attached
08:41 - 09:00
Talk
Conversations on Analysis 4
Paper Presentations
David TrabishTel Aviv University, Israel, Dominik HelmTU Darmstadt, Germany, Rafi ShalomTel Aviv University, Israel, Rongchen XuTsinghua University, China, Shahar MaozTel Aviv University, Israel, M: Rachel Tzoref-BrillIBM Research