Trace-based verification of imperative programs with I/O

Gregory Malecha and Greg Morrisett and Ryan Wisnesky

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.

ynot separation logic coq verification

download publisher's link

Citation (BibTex)

@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."
}