@article{Malecha201195,
  title = "Trace-based verification of imperative programs with I/O ",
  journal = "Journal of Symbolic Computation ",
  volume = "46",
  number = "2",
  pages = "95 - 118",
  year = "2011",
  note = "Automated Specification and Verification of Web Systems ",
  issn = "0747-7171",
  doi = "http://dx.doi.org/10.1016/j.jsc.2010.08.004",
  url = "http://www.sciencedirect.com/science/article/pii/S0747717110001343",
  author = "Gregory Malecha and Greg Morrisett and Ryan Wisnesky",
  keywords = "Program verification",
  keywords = "Separation logic",
  keywords = "Dependent types",
  keywords = "Traces",
  keywords = "Imperative programming",
  keywords = "Ynot ",
  abstract = "In this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers, files, and socket I/O with respect to high level I/O protocol descriptions by using the Coq proof assistant. We present a web-based course gradebook application developed with Ynot, a Coq library for verified imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynot’s underlying Hoare logic with event traces to reason about I/O and protocol behavior. Expressive abstractions allow the modular verification of both high level specifications like privacy guarantees and low level properties like data structure pointer invariants."
}