Anuncio: Trace-based verification of imperative programs with I/O
Gregory Malecha, Greg Morrisett y Ryan Wisnesky han publicado el artículo Trace-based verification of imperative programs with I/O en el Journal of Symbolic Computation. Una versión del artículo puede leerse aquí.
El resumen del artículo es
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.
Los autores son miembros del Grupo de Lenguajes de Programación de la Universidad de Harvard.
Este artículo está relacionado con el proyecto SAFE (Semantically Aware Foundation Environment) comentado en una entrada anterior.