SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 09:40 - 10:00 at SPLASH-III - F-2B Chair(s): Hridesh Rajan
Fri 20 Nov 2020 21:40 - 22:00 at SPLASH-III - F-2B Chair(s): Steve Blackburn, Alex Potanin

We present Deuterium—a framework for implementing Java methods as executable contracts. Deuterium introduces a novel, type-safe way to write method contracts entirely in Java, as a combination of imperative generators and declarative specifications (written in a first-order relational logic with transitive closure). Existing approaches are typically based on encoding both the specification and the program heap into a constraint language, and then using an off-the-shelf constraint solver—without any additional guidance—to search for a new program heap that satisfies the specification. Deuterium takes advantage of user-provided generators to prune the search space and reduce incurred overhead of constraint solving. Deuterium supports two ways of solving declarative constraints: SAT-based and search-based with in-memory state exploration. We evaluate our approach on a suite of data structures, established as a standard benchmark by prior work. Furthermore, we use random and sequence-based test generation to create a new benchmark designed to mimic realistic execution scenarios. Our results show that generators improve the performance of executable contracts and that in-memory state exploration is the algorithm of choice when heap sizes are small.

Fri 20 Nov

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

09:00 - 10:20
F-2BOOPSLA at SPLASH-III +12h
Chair(s): Hridesh Rajan Iowa State University, USA
09:00
20m
Talk
Feedback-Driven Semi-supervised Synthesis of Program Transformations
OOPSLA
Xiang Gao National University of Singapore, Shraddha Barke University of California at San Diego, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Sumit Gulwani Microsoft, Alan Leung Microsoft, Nachiappan Nagappan Microsoft Research, Ashish Tiwari Microsoft
Link to publication DOI Media Attached
09:20
20m
Talk
Testing Differential Privacy with Dual Interpreters
OOPSLA
Hengchu Zhang University of Pennsylvania, Edo Roth University of Pennsylvania, Andreas Haeberlen University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Aaron Roth University of Pennsylvania
Link to publication DOI Media Attached
09:40
20m
Talk
Unifying Execution of Imperative Generators and Declarative Specifications
OOPSLA
Pengyu Nie University of Texas at Austin, Marinela Parovic University of Texas at Austin, Zhiqiang Zang University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin, Aleksandar Milicevic Microsoft, Milos Gligoric University of Texas at Austin
Link to publication DOI Media Attached
10:00
20m
Talk
Differentially-Private Software Frequency Profiling under Linear Constraints
OOPSLA
Hailong Zhang Fordham University, Yu Hao Ohio State University, Sufian Latif Ohio State University, Raef Bassily Ohio State University, Atanas Rountev Ohio State University
Link to publication DOI Media Attached
21:00 - 22:20
F-2BOOPSLA at SPLASH-III
Chair(s): Steve Blackburn Australian National University, Alex Potanin Victoria University of Wellington
21:00
20m
Talk
Feedback-Driven Semi-supervised Synthesis of Program Transformations
OOPSLA
Xiang Gao National University of Singapore, Shraddha Barke University of California at San Diego, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Sumit Gulwani Microsoft, Alan Leung Microsoft, Nachiappan Nagappan Microsoft Research, Ashish Tiwari Microsoft
Link to publication DOI Media Attached
21:20
20m
Talk
Testing Differential Privacy with Dual Interpreters
OOPSLA
Hengchu Zhang University of Pennsylvania, Edo Roth University of Pennsylvania, Andreas Haeberlen University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Aaron Roth University of Pennsylvania
Link to publication DOI Media Attached
21:40
20m
Talk
Unifying Execution of Imperative Generators and Declarative Specifications
OOPSLA
Pengyu Nie University of Texas at Austin, Marinela Parovic University of Texas at Austin, Zhiqiang Zang University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin, Aleksandar Milicevic Microsoft, Milos Gligoric University of Texas at Austin
Link to publication DOI Media Attached
22:00
20m
Talk
Differentially-Private Software Frequency Profiling under Linear Constraints
OOPSLA
Hailong Zhang Fordham University, Yu Hao Ohio State University, Sufian Latif Ohio State University, Raef Bassily Ohio State University, Atanas Rountev Ohio State University
Link to publication DOI Media Attached