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): Alex Potanin, Steve Blackburn

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
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20: F-2BOOPSLA at SPLASH-III +12h
Chair(s): Hridesh RajanIowa State University, USA
09:00 - 09:20
Talk
OOPSLA
Xiang GaoNational University of Singapore, Shraddha BarkeUniversity of California at San Diego, Arjun RadhakrishnaMicrosoft, Gustavo SoaresMicrosoft, Sumit GulwaniMicrosoft, Alan LeungMicrosoft, Nachiappan NagappanMicrosoft Research, Ashish TiwariMicrosoft
Link to publication DOI Media Attached
09:20 - 09:40
Talk
OOPSLA
Hengchu ZhangUniversity of Pennsylvania, Edo RothUniversity of Pennsylvania, Andreas HaeberlenUniversity of Pennsylvania, Benjamin C. PierceUniversity of Pennsylvania, Aaron RothUniversity of Pennsylvania
Link to publication DOI Media Attached
09:40 - 10:00
Talk
OOPSLA
Pengyu NieUniversity of Texas at Austin, Marinela ParovicUniversity of Texas at Austin, Zhiqiang ZangUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin, Aleksandar MilicevicMicrosoft, Milos GligoricUniversity of Texas at Austin
Link to publication DOI Media Attached
10:00 - 10:20
Talk
OOPSLA
Hailong ZhangFordham University, Yu HaoOhio State University, Sufian LatifOhio State University, Raef BassilyOhio State University, Atanas RountevOhio State University
Link to publication DOI Media Attached
21:00 - 22:20: F-2BOOPSLA at SPLASH-III
Chair(s): Alex PotaninVictoria University of Wellington, Steve BlackburnAustralian National University
21:00 - 21:20
Talk
OOPSLA
Xiang GaoNational University of Singapore, Shraddha BarkeUniversity of California at San Diego, Arjun RadhakrishnaMicrosoft, Gustavo SoaresMicrosoft, Sumit GulwaniMicrosoft, Alan LeungMicrosoft, Nachiappan NagappanMicrosoft Research, Ashish TiwariMicrosoft
Link to publication DOI Media Attached
21:20 - 21:40
Talk
OOPSLA
Hengchu ZhangUniversity of Pennsylvania, Edo RothUniversity of Pennsylvania, Andreas HaeberlenUniversity of Pennsylvania, Benjamin C. PierceUniversity of Pennsylvania, Aaron RothUniversity of Pennsylvania
Link to publication DOI Media Attached
21:40 - 22:00
Talk
OOPSLA
Pengyu NieUniversity of Texas at Austin, Marinela ParovicUniversity of Texas at Austin, Zhiqiang ZangUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin, Aleksandar MilicevicMicrosoft, Milos GligoricUniversity of Texas at Austin
Link to publication DOI Media Attached
22:00 - 22:20
Talk
OOPSLA
Hailong ZhangFordham University, Yu HaoOhio State University, Sufian LatifOhio State University, Raef BassilyOhio State University, Atanas RountevOhio State University
Link to publication DOI Media Attached