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
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101782
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:06:06 AM
Last modification on : Wednesday, May 22, 2019 - 1:32:15 AM

File

RR1993-08.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101782, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

10

Files downloads

6