Certified Web Services in Ynot
View/ Open
Published Version
http://www.risc.uni-linz.ac.at/about/conferences/wwv09/Metadata
Show full item recordCitation
Wisnesky, Ryan, Gregory Malecha, and Greg Morrisett. 2009. Certified Web Services in Ynot. In Proceedings, 5th International Workshop on Automated Specification and Verification of Web Systems: July 17, 2009, Castle of Hagenberg, Austria.Abstract
In this paper we demonstrate that it is possible to implement certi ed web systems in a way not much di erent from writingStandard ML or Haskell code, including use of imperative features like pointers, les, and socket I/O. We present a web-based course gradebook application developed with Ynot, a Coq library for certi ed 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 be- havior. Expressive abstractions allow the modular certi cation of both high level speci cations like privacy guarantees and low level properties like memory safety and correct parsing.
Other Sources
http://ynot.cs.harvard.edu/papers/wwv09.pdfTerms of Use
This article is made available under the terms and conditions applicable to Open Access Policy Articles, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#OAPCitable link to this page
http://nrs.harvard.edu/urn-3:HUL.InstRepos:3980868
Collections
- FAS Scholarly Articles [18292]
Contact administrator regarding this item (to report mistakes or request changes)