SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 10:50 - 11:05 at Zurich D - Specification Synthesis Chair(s): Zoe Paraskevopoulou
Thu 21 Oct 2021 18:50 - 19:05 at Zurich D - Specification Synthesis - mirror Chair(s): Toby Murray

Being able to detect program runtime complexity is useful in many tasks (e.g., checking expected performance and identifying potential security vulnerabilities).
In this work, we introduce a new dynamic approach for inferring the asymptotic complexity bounds of recursive programs.
From program execution traces, we learn \emph{recurrence relations} and solve them using pattern matching to obtain closed-form solutions representing the complexity bounds of the program.
This approach allows us to efficiently infer simple recurrence relations that represent nontrivial, potentially nonlinear polynomial and non-polynomial, complexity bounds.

We present Dynaplex, a tool that implements these ideas to automatically generate recurrence relations from execution traces.
Our preliminary results on popular and challenging recursive programs show that Dynaplex can learn precise relations capturing worst-case complexity bounds (e.g., $O(n \log n)$ for mergesort, $O(2^n)$ for Tower of Hanoi and $O(n^{1.58})$ for Karatsuba's multiplication algorithm).

Thu 21 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
Specification SynthesisOOPSLA at Zurich D +8h
Chair(s): Zoe Paraskevopoulou Northeastern University
10:50
15m
Talk
Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence RelationsVirtual
OOPSLA
Didier Ishimwe University of Nebraska-Lincoln, KimHao Nguyen University of Nebraska-Lincoln, ThanhVu Nguyen George Mason University
DOI
11:05
15m
Talk
Static Detection of Silent Misconfigurations with Deep Interaction AnalysisIn-Person
OOPSLA
Jialu Zhang Yale University, Ruzica Piskac Yale University, Ennan Zhai Alibaba Group, Tianyin Xu University of Illinois at Urbana-Champaign
DOI
11:20
15m
Talk
Data-Driven Abductive Inference of Library SpecificationsIn-Person
OOPSLA
Zhe Zhou Purdue University, Robert Dickerson Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
DOI
11:35
15m
Talk
Synthesizing Contracts Correct Modulo a Test GeneratorIn-Person
OOPSLA
Angello Astorga University of Illinois at Urbana-Champaign, Shambwaditya Saha Tufts University, Ahmad Dinkins University of Illinois at Urbana-Champaign, Felicia Wang University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Tao Xie Peking University
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA

18:50 - 20:10
Specification Synthesis - mirrorOOPSLA at Zurich D
Chair(s): Toby Murray University of Melbourne
18:50
15m
Talk
Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence RelationsVirtual
OOPSLA
Didier Ishimwe University of Nebraska-Lincoln, KimHao Nguyen University of Nebraska-Lincoln, ThanhVu Nguyen George Mason University
DOI
19:05
15m
Talk
Static Detection of Silent Misconfigurations with Deep Interaction AnalysisIn-Person
OOPSLA
Jialu Zhang Yale University, Ruzica Piskac Yale University, Ennan Zhai Alibaba Group, Tianyin Xu University of Illinois at Urbana-Champaign
DOI
19:20
15m
Talk
Data-Driven Abductive Inference of Library SpecificationsIn-Person
OOPSLA
Zhe Zhou Purdue University, Robert Dickerson Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
DOI
19:35
15m
Talk
Synthesizing Contracts Correct Modulo a Test GeneratorIn-Person
OOPSLA
Angello Astorga University of Illinois at Urbana-Champaign, Shambwaditya Saha Tufts University, Ahmad Dinkins University of Illinois at Urbana-Champaign, Felicia Wang University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Tao Xie Peking University
DOI
19:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA