@article{Kincaid:2017:NRI:3177123.3158142,
    Address = {New York, NY, USA},
    Author = {Kincaid, Zachary and Cyphert, John and Breck, Jason and Reps, Thomas},
    File = {popl18a (0) - a - a - g.pdf},
    ISSN = {2475-1421},
    Journal = {Proc. ACM Program. Lang.},
    Keywords = {Invariant generation, Operational calculus, Recurrence relation},
    Month = {December},
    Number = {POPL},
    Pages = {54:1--54:33},
    Publisher = {ACM},
    Title = {Non-linear Reasoning for Invariant Synthesis},
    URL = {http://doi.acm.org/10.1145/3158142},
    Volume = {2},
    Year = {2017},
    acmid = {3158142},
    articleno = {54},
    bdsk-url-1 = {http://doi.acm.org/10.1145/3158142},
    bdsk-url-2 = {https://doi.org/10.1145/3158142},
    date-added = {2018-07-19 15:57:26 +0000},
    date-modified = {2018-07-19 15:57:26 +0000},
    issue_date = {January 2018},
    numpages = {33},
    doi = {10.1145/3158142}
}

@article{Kincaid:2017:NRI:3177123.3158142, Address = {New York, NY, USA}, Author = {Kincaid, Zachary and Cyphert, John and Breck, Jason and Reps, Thomas}, File = {popl18a (0) - a - a - g.pdf}, ISSN = {2475-1421}, Journal = {Proc. ACM Program. Lang.}, Keywords = {Invariant generation, Operational calculus, Recurrence relation}, Month = {December}, Number = {POPL}, Pages = {54:1--54:33}, Publisher = {ACM}, Title = {Non-linear Reasoning for Invariant Synthesis}, URL = {http://doi.acm.org/10.1145/3158142}, Volume = {2}, Year = {2017}, acmid = {3158142}, articleno = {54}, bdsk-url-1 = {http://doi.acm.org/10.1145/3158142}, bdsk-url-2 = {https://doi.org/10.1145/3158142}, date-added = {2018-07-19 15:57:26 +0000}, date-modified = {2018-07-19 15:57:26 +0000}, issue_date = {January 2018}, numpages = {33}, doi = {10.1145/3158142} }