@article{Malecha_2011,
    doi = {10.1016/j.jsc.2010.08.004},
    url = {https://doi.org/10.1016%2Fj.jsc.2010.08.004},
    year = {2011},
    month = {feb},
    publisher = {Elsevier {BV}},
    volume = {46},
    number = {2},
    pages = {95--118},
    author = {Gregory Malecha and Greg Morrisett and Ryan Wisnesky},
    title = {Trace-based verification of imperative programs with I/O},
    journal = {Journal of Symbolic Computation}
}

@article{Malecha_2011, doi = {10.1016/j.jsc.2010.08.004}, url = {https://doi.org/10.1016%2Fj.jsc.2010.08.004}, year = {2011}, month = {feb}, publisher = {Elsevier {BV}}, volume = {46}, number = {2}, pages = {95--118}, author = {Gregory Malecha and Greg Morrisett and Ryan Wisnesky}, title = {Trace-based verification of imperative programs with I/O}, journal = {Journal of Symbolic Computation} }