Trace-based verification of imperative programs with I/O
In: Journal of Symbolic Computation, Jg. 46 (2011-02-01), Heft 2, S. 95-118
Online
academicJournal
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. [ABSTRACT FROM AUTHOR]
Titel: |
Trace-based verification of imperative programs with I/O
|
---|---|
Autor/in / Beteiligte Person: | Malecha, Gregory ; Morrisett, Greg ; Wisnesky, Ryan |
Link: | |
Zeitschrift: | Journal of Symbolic Computation, Jg. 46 (2011-02-01), Heft 2, S. 95-118 |
Veröffentlichung: | 2011 |
Medientyp: | academicJournal |
ISSN: | 0747-7171 (print) |
DOI: | 10.1016/j.jsc.2010.08.004 |
Schlagwort: |
|
Sonstiges: |
|