@inproceedings{nie2020unifying,
author = {Nie, Pengyu and Parovic, Marinela and Zang, Zhiqiang and Khurshid, Sarfraz and Milicevic, Aleksandar and Gligoric, Milos},
title = {Unifying execution of imperative generators and declarative specifications},
booktitle = {PLDI 2022},
year = {2020},
month = {November},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/unifying-execution-of-imperative-generators-and-declarative-specifications/},
}