(OOPSLA 2020) Unifying Execution of Imperative Generators and Declarative Specifications
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 JunDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 16:50 | |||
15:30 20mTalk | (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 20mTalk | (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 20mTalk | (PLDI 2021) Logical Bytecode Reduction SIGPLAN Track Christian Gram Kalhauge Technical University of Denmark, Jens Palsberg University of California, Los Angeles (UCLA) | ||
16:30 20mTalk | (PLDI 2021) Quantum abstract interpretation SIGPLAN Track Link to publication DOI Authorizer link Pre-print |