SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Thu 26 Oct 2023 17:12 - 17:30 at Room II - program analysis 2 Chair(s): Annette Bieniusa

Oracle-guided inductive synthesis (OGIS) is a widely-used framework to apply program synthesis techniques in practice. The question selection problem aims at reducing the number of iterations in OGIS by selecting a proper input for each OGIS iteration. Theoretically, a question selector can generally improve the performance of OGIS solvers on both interactive and non-interactive tasks if it is not only effective for reducing iterations but also efficient. However, all existing effective question selectors fail in satisfying the requirement of efficiency. To ensure effectiveness, they convert the question selection problem into an optimization one, which is difficult to solve within a short time.

In this paper, we propose a novel question selector, named \textit{LearnSy}. \textit{LearnSy} is both efficient and effective and thus achieves general improvement for OGIS solvers for the first time. Since we notice that the optimization tasks in previous studies are difficult because of the complex behavior of operators, we estimate these behaviors in \textit{LearnSy} as simple random events. Subsequently, we provide theoretical results for the precision of this estimation and design an efficient algorithm for its calculation.

According to our evaluation, when dealing with interactive tasks, \textit{LearnSy} can offer competitive performance compared to existing selectors while being more efficient and more general. Moreover, when working on non-interactive tasks, \textit{LearnSy} can generally reduce the time cost of existing CEGIS solvers by up to $43.0%$.

Thu 26 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
program analysis 2OOPSLA at Room II
Chair(s): Annette Bieniusa University of Kaiserslautern-Landau
16:00
18m
Talk
Historia: Refuting Callback Reachability with Message-History Logics
OOPSLA
Shawn Meier University of Colorado at Boulder, Sergio Mover École Polytechnique, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon
DOI
16:18
18m
Talk
Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis
OOPSLA
Giovanna Kobus Conrado Hong Kong University of Science and Technology, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Kerim Kochekov Hong Kong University of Science and Technology, Yun Chen Tsai Hong Kong University of Science and Technology, Ahmed Khaled Zaher Hong Kong University of Science and Technology
DOI
16:36
18m
Talk
A Cocktail Approach to Practical Call Graph Construction
OOPSLA
Yuandao Cai Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology
DOI
16:54
18m
Talk
Building Dynamic System Call Sandbox with Partial Order Analysis
OOPSLA
Quan Zhang Tsinghua University, Chijin Zhou Tsinghua University, Yiwen Xu Tsinghua University, Zijing Yin Tsinghua University, Mingzhe Wang Tsinghua University, Zhuo Su Tsinghua University, Chengnian Sun University of Waterloo, Yu Jiang Tsinghua University, Jiaguang Sun Tsinghua University
DOI
17:12
18m
Talk
Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection
OOPSLA
Ruyi Ji Peking University, Chaozhe Kong Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
DOI