Thu 16 Jun 2022 15:50 - 16:10 at Cockatoo - Testing Chair(s): Yu Feng

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 the advantage of user-provided generators to prune the search space and reduce incurred overhead of constraint solving. Deuterium supports two ways to 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 more realistic execution scenarios. Our results show that generators improve performance of executable contracts and that in-memory state exploration is the algorithm of choice when heap sizes are small.

Thu 16 Jun

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

15:30 - 16:50
TestingSIGPLAN Track at Cockatoo
Chair(s): Yu Feng University of California, Santa Barbara
15:30
20m
Talk
(OOPSLA 2020) A Model for Detecting Faults in Build Specifications
SIGPLAN Track
Thodoris Sotiropoulos Athens University of Economics and Business, Stefanos Chaliasos Imperial College London, Dimitris Mitropoulos University of Athens, Diomidis Spinellis Athens University of Economics and Business & Delft University of Technology
15:50
20m
Talk
(OOPSLA 2020) Unifying Execution of Imperative Generators and Declarative Specifications
SIGPLAN Track
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
16:10
20m
Talk
(PLDI 2021) Logical Bytecode Reduction
SIGPLAN Track
Christian Gram Kalhauge Technical University of Denmark, Jens Palsberg University of California, Los Angeles (UCLA)
16:30
20m
Talk
(PLDI 2021) Quantum abstract interpretation
SIGPLAN Track
Nengkun Yu UTS, Jens Palsberg University of California, Los Angeles (UCLA)
Link to publication DOI Authorizer link Pre-print