A framework for parallel program refinement

J.P. Bodeveix
M. Filali

In TACAS, pages 159--173

Abstract:

This paper presents a formal framework for developing provably correct parallel programs through refinements. We formalize rigorously, with respect to typing, some imperative programming constructs and propose refinements of them. Moreover, we try to make the semantics denotation as close as possible to the usual programming notation; the aim being to make easy the reasoning at the semantics level. This formalization is embedded within the HOL interactive theorem prover and consequently reusable as a framework for general programming by refinement.

Comments
IRIT, Toulouse, France.

Available as PostScript.

BRICS WWW home page