@inproceedings{Leino:2012:PEJ:2384616.2384646, author = {Leino, K. Rustan M. and Milicevic, Aleksandar}, title = {Program extrapolation with jennisys}, booktitle = {Proceedings of the ACM international conference on Object oriented programming systems languages and applications}, series = {OOPSLA '12}, year = {2012}, isbn = {978-1-4503-1561-6}, location = {Tucson, Arizona, USA}, pages = {411--430}, numpages = {20}, url = {http://doi.acm.org/10.1145/2384616.2384646}, doi = {10.1145/2384616.2384646}, acmid = {2384646}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {abstract specifications, concrete representations, coupling invariants, dafny, jennisys, postconditions, preconditions, program synthesis}, }