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

Programmers often leverage data structure libraries that provide
useful and reusable abstractions. Modular verification of programs
that make use of these libraries naturally rely on specifications
that capture important properties about how the library expects
these data structures to be accessed and manipulated. However,
these specifications are often missing or incomplete, making it hard
for clients to be confident they are using the library safely. When
library source code is also unavailable, as is often the case, the
challenge to infer meaningful specifications is further exacerbated.
In this paper, we present a novel data-driven abductive inference
mechanism that infers specifications for library methods sufficient
to enable verification of the library's clients. Our
technique combines a data-driven learning-based framework to
postulate candidate specifications, along with SMT-provided
counterexamples to refine these candidates, taking special care to
prevent generating specifications that overfit to sampled tests.
The resulting specifications form a minimal set of requirements on
the behavior of library implementations that ensures safety of a
particular client program. Our solution thus provides a new
multi-abduction procedure for precise specification inference of
data structure libraries guided by client-side verification tasks.
Experimental results on a wide range of realistic OCaml data
structure programs demonstrate the effectiveness of the approach.

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