Axiomatic Semantics of Data-Parallel Languages; Automatization of Programs Verification

We give a Hoare-like proof system for the data-parallel language L, and we present an automatic tool to aid program correctness proof. After recalling L's operational semantics, we define an axiomatic semantics. We illustrate proof of L programs with two examples. Then we extend our semantics to weakest precondition, and we deduce techniques for mechanizing program verification from Gordon's verification condition method. We prove its correctness, and we present an implementation of this method in the CENTAUR system.Nous présentons un système de preuve à la Hoare pour le langage à parallélisme de donnée L, ainsi qu'une automatisation possible de la preuve de programmes; Dans un premier temps nous définissons une sémantique axiomatique de L, après un rappel de sa sémantique opérationnelle. Nous illustrons son application à la preuve de programmes sur deux exemples,dont un non trivial. Ensuite, après avoir étendu notre sémantique aux pré-conditions les plus faibles, nous déduisons une mécanisation de la preuve de programmes inspirée des vérification condition de Gordon. Nous prouvons alors sa correction. Nous présentons enfin son implémentation sous l'atelier sémantique CENTAU