Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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

Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:06:06 AM
Last modification on : Wednesday, October 26, 2022 - 8:15:44 AM


Files produced by the author(s)


  • HAL Id : hal-02101782, version 1



V. Mounier, Gil Utard. Axiomatic Semantics of Data-Parallel Languages; Automatization of Programs Verification. [Research Report] LIP RR-1993-08, Laboratoire de l'informatique du parallélisme. 1993, 2+48p. ⟨hal-02101782⟩



Record views


Files downloads